Proof of Theorem wopprc
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . . . . . . 9
⊢
({∅} = {{𝐴},
∅} → {∅} = {{𝐴}, ∅}) | 
| 2 |  | dfsn2 4638 | . . . . . . . . 9
⊢ {∅}
= {∅, ∅} | 
| 3 | 1, 2 | eqtr3di 2791 | . . . . . . . 8
⊢
({∅} = {{𝐴},
∅} → {{𝐴},
∅} = {∅, ∅}) | 
| 4 |  | snex 5435 | . . . . . . . . 9
⊢ {𝐴} ∈ V | 
| 5 |  | 0ex 5306 | . . . . . . . . 9
⊢ ∅
∈ V | 
| 6 | 4, 5 | preqr1 4847 | . . . . . . . 8
⊢ ({{𝐴}, ∅} = {∅, ∅}
→ {𝐴} =
∅) | 
| 7 | 3, 6 | syl 17 | . . . . . . 7
⊢
({∅} = {{𝐴},
∅} → {𝐴} =
∅) | 
| 8 |  | snprc 4716 | . . . . . . 7
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) | 
| 9 | 7, 8 | sylibr 234 | . . . . . 6
⊢
({∅} = {{𝐴},
∅} → ¬ 𝐴
∈ V) | 
| 10 | 8 | biimpi 216 | . . . . . . . 8
⊢ (¬
𝐴 ∈ V → {𝐴} = ∅) | 
| 11 | 10 | preq1d 4738 | . . . . . . 7
⊢ (¬
𝐴 ∈ V → {{𝐴}, ∅} = {∅,
∅}) | 
| 12 | 2, 11 | eqtr4id 2795 | . . . . . 6
⊢ (¬
𝐴 ∈ V → {∅}
= {{𝐴},
∅}) | 
| 13 | 9, 12 | impbii 209 | . . . . 5
⊢
({∅} = {{𝐴},
∅} ↔ ¬ 𝐴
∈ V) | 
| 14 | 13 | con2bii 357 | . . . 4
⊢ (𝐴 ∈ V ↔ ¬ {∅}
= {{𝐴},
∅}) | 
| 15 |  | snprc 4716 | . . . . . . 7
⊢ (¬
𝐵 ∈ V ↔ {𝐵} = ∅) | 
| 16 |  | eqcom 2743 | . . . . . . 7
⊢ ({𝐵} = ∅ ↔ ∅ =
{𝐵}) | 
| 17 | 15, 16 | bitr2i 276 | . . . . . 6
⊢ (∅
= {𝐵} ↔ ¬ 𝐵 ∈ V) | 
| 18 | 17 | con2bii 357 | . . . . 5
⊢ (𝐵 ∈ V ↔ ¬ ∅ =
{𝐵}) | 
| 19 | 5 | sneqr 4839 | . . . . . 6
⊢
({∅} = {{𝐵}}
→ ∅ = {𝐵}) | 
| 20 |  | sneq 4635 | . . . . . 6
⊢ (∅
= {𝐵} → {∅} =
{{𝐵}}) | 
| 21 | 19, 20 | impbii 209 | . . . . 5
⊢
({∅} = {{𝐵}}
↔ ∅ = {𝐵}) | 
| 22 | 18, 21 | xchbinxr 335 | . . . 4
⊢ (𝐵 ∈ V ↔ ¬ {∅}
= {{𝐵}}) | 
| 23 | 14, 22 | anbi12i 628 | . . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}})) | 
| 24 |  | pm4.56 990 | . . . 4
⊢ ((¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}}) ↔ ¬ ({∅} = {{𝐴}, ∅} ∨ {∅} =
{{𝐵}})) | 
| 25 |  | snex 5435 | . . . . 5
⊢ {∅}
∈ V | 
| 26 | 25 | elpr 4649 | . . . 4
⊢
({∅} ∈ {{{𝐴}, ∅}, {{𝐵}}} ↔ ({∅} = {{𝐴}, ∅} ∨ {∅} = {{𝐵}})) | 
| 27 | 24, 26 | xchbinxr 335 | . . 3
⊢ ((¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}}) ↔ ¬ {∅} ∈ {{{𝐴}, ∅}, {{𝐵}}}) | 
| 28 | 23, 27 | bitri 275 | . 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬
{∅} ∈ {{{𝐴},
∅}, {{𝐵}}}) | 
| 29 |  | df1o2 8514 | . . 3
⊢
1o = {∅} | 
| 30 | 29 | eleq1i 2831 | . 2
⊢
(1o ∈ {{{𝐴}, ∅}, {{𝐵}}} ↔ {∅} ∈ {{{𝐴}, ∅}, {{𝐵}}}) | 
| 31 | 28, 30 | xchbinxr 335 | 1
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬
1o ∈ {{{𝐴},
∅}, {{𝐵}}}) |