Step | Hyp | Ref
| Expression |
1 | | difsnss 3510 |
. . 3
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴) |
2 | 1 | adantl 262 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) ⊆ 𝐴) |
3 | | simpr 103 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) |
4 | | velsn 3392 |
. . . . . . 7
⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) |
5 | 3, 4 | sylibr 137 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑥 ∈ {𝐵}) |
6 | | elun2 3111 |
. . . . . 6
⊢ (𝑥 ∈ {𝐵} → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
7 | 5, 6 | syl 14 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
8 | | simplr 482 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ 𝐴) |
9 | | simpr 103 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 = 𝐵) |
10 | 9, 4 | sylnibr 602 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐵}) |
11 | 8, 10 | eldifd 2928 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴 ∖ {𝐵})) |
12 | | elun1 3110 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∖ {𝐵}) → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
14 | | simpr 103 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
15 | | simpll 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐴 ∈ ω) |
16 | | elnn 4328 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐴 ∈ ω) → 𝑥 ∈ ω) |
17 | 14, 15, 16 | syl2anc 391 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ω) |
18 | | simplr 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐴) |
19 | | elnn 4328 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝐴 ∧ 𝐴 ∈ ω) → 𝐵 ∈ ω) |
20 | 18, 15, 19 | syl2anc 391 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ω) |
21 | | nndceq 6077 |
. . . . . . 7
⊢ ((𝑥 ∈ ω ∧ 𝐵 ∈ ω) →
DECID 𝑥 =
𝐵) |
22 | 17, 20, 21 | syl2anc 391 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → DECID 𝑥 = 𝐵) |
23 | | df-dc 743 |
. . . . . 6
⊢
(DECID 𝑥 = 𝐵 ↔ (𝑥 = 𝐵 ∨ ¬ 𝑥 = 𝐵)) |
24 | 22, 23 | sylib 127 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐵 ∨ ¬ 𝑥 = 𝐵)) |
25 | 7, 13, 24 | mpjaodan 711 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
26 | 25 | ex 108 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵}))) |
27 | 26 | ssrdv 2951 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) |
28 | 2, 27 | eqssd 2962 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |