Proof of Theorem wopprc
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . 9
⊢
({∅} = {{𝐴},
∅} → {∅} = {{𝐴}, ∅}) |
2 | | dfsn2 4579 |
. . . . . . . . 9
⊢ {∅}
= {∅, ∅} |
3 | 1, 2 | eqtr3di 2794 |
. . . . . . . 8
⊢
({∅} = {{𝐴},
∅} → {{𝐴},
∅} = {∅, ∅}) |
4 | | snex 5357 |
. . . . . . . . 9
⊢ {𝐴} ∈ V |
5 | | 0ex 5234 |
. . . . . . . . 9
⊢ ∅
∈ V |
6 | 4, 5 | preqr1 4784 |
. . . . . . . 8
⊢ ({{𝐴}, ∅} = {∅, ∅}
→ {𝐴} =
∅) |
7 | 3, 6 | syl 17 |
. . . . . . 7
⊢
({∅} = {{𝐴},
∅} → {𝐴} =
∅) |
8 | | snprc 4658 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
9 | 7, 8 | sylibr 233 |
. . . . . 6
⊢
({∅} = {{𝐴},
∅} → ¬ 𝐴
∈ V) |
10 | 8 | biimpi 215 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V → {𝐴} = ∅) |
11 | 10 | preq1d 4680 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → {{𝐴}, ∅} = {∅,
∅}) |
12 | 2, 11 | eqtr4id 2798 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → {∅}
= {{𝐴},
∅}) |
13 | 9, 12 | impbii 208 |
. . . . 5
⊢
({∅} = {{𝐴},
∅} ↔ ¬ 𝐴
∈ V) |
14 | 13 | con2bii 357 |
. . . 4
⊢ (𝐴 ∈ V ↔ ¬ {∅}
= {{𝐴},
∅}) |
15 | | snprc 4658 |
. . . . . . 7
⊢ (¬
𝐵 ∈ V ↔ {𝐵} = ∅) |
16 | | eqcom 2746 |
. . . . . . 7
⊢ ({𝐵} = ∅ ↔ ∅ =
{𝐵}) |
17 | 15, 16 | bitr2i 275 |
. . . . . 6
⊢ (∅
= {𝐵} ↔ ¬ 𝐵 ∈ V) |
18 | 17 | con2bii 357 |
. . . . 5
⊢ (𝐵 ∈ V ↔ ¬ ∅ =
{𝐵}) |
19 | 5 | sneqr 4776 |
. . . . . 6
⊢
({∅} = {{𝐵}}
→ ∅ = {𝐵}) |
20 | | sneq 4576 |
. . . . . 6
⊢ (∅
= {𝐵} → {∅} =
{{𝐵}}) |
21 | 19, 20 | impbii 208 |
. . . . 5
⊢
({∅} = {{𝐵}}
↔ ∅ = {𝐵}) |
22 | 18, 21 | xchbinxr 334 |
. . . 4
⊢ (𝐵 ∈ V ↔ ¬ {∅}
= {{𝐵}}) |
23 | 14, 22 | anbi12i 626 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}})) |
24 | | pm4.56 985 |
. . . 4
⊢ ((¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}}) ↔ ¬ ({∅} = {{𝐴}, ∅} ∨ {∅} =
{{𝐵}})) |
25 | | snex 5357 |
. . . . 5
⊢ {∅}
∈ V |
26 | 25 | elpr 4589 |
. . . 4
⊢
({∅} ∈ {{{𝐴}, ∅}, {{𝐵}}} ↔ ({∅} = {{𝐴}, ∅} ∨ {∅} = {{𝐵}})) |
27 | 24, 26 | xchbinxr 334 |
. . 3
⊢ ((¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}}) ↔ ¬ {∅} ∈ {{{𝐴}, ∅}, {{𝐵}}}) |
28 | 23, 27 | bitri 274 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬
{∅} ∈ {{{𝐴},
∅}, {{𝐵}}}) |
29 | | df1o2 8293 |
. . 3
⊢
1o = {∅} |
30 | 29 | eleq1i 2830 |
. 2
⊢
(1o ∈ {{{𝐴}, ∅}, {{𝐵}}} ↔ {∅} ∈ {{{𝐴}, ∅}, {{𝐵}}}) |
31 | 28, 30 | xchbinxr 334 |
1
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬
1o ∈ {{{𝐴},
∅}, {{𝐵}}}) |