Step | Hyp | Ref
| Expression |
1 | | difsnss 3531 |
. . 3
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴) |
2 | 1 | adantl 271 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴) |
3 | | simpr 108 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) |
4 | | velsn 3415 |
. . . . . . 7
⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) |
5 | 3, 4 | sylibr 132 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑥 ∈ {𝐵}) |
6 | | elun2 3140 |
. . . . . 6
⊢ (𝑥 ∈ {𝐵} → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
7 | 5, 6 | syl 14 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
8 | | simplr 496 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ 𝐴) |
9 | | simpr 108 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 = 𝐵) |
10 | 9, 4 | sylnibr 634 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐵}) |
11 | 8, 10 | eldifd 2983 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴 ∖ {𝐵})) |
12 | | elun1 3139 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
14 | | simpr 108 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
15 | | simpll 495 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ ω) |
16 | | elnn 4346 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ ω) → 𝑥 ∈ ω) |
17 | 14, 15, 16 | syl2anc 403 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ω) |
18 | | simplr 496 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐴) |
19 | | elnn 4346 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐴 ∈ ω) → 𝐵 ∈ ω) |
20 | 18, 15, 19 | syl2anc 403 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ω) |
21 | | nndceq 6100 |
. . . . . . 7
⊢ ((𝑥 ∈ ω ∧ 𝐵 ∈ ω) →
DECID 𝑥 =
𝐵) |
22 | 17, 20, 21 | syl2anc 403 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → DECID 𝑥 = 𝐵) |
23 | | df-dc 776 |
. . . . . 6
⊢
(DECID 𝑥 = 𝐵 ↔ (𝑥 = 𝐵 ∨ ¬ 𝑥 = 𝐵)) |
24 | 22, 23 | sylib 120 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐵 ∨ ¬ 𝑥 = 𝐵)) |
25 | 7, 13, 24 | mpjaodan 744 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
26 | 25 | ex 113 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))) |
27 | 26 | ssrdv 3005 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
28 | 2, 27 | eqssd 3016 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |