Proof of Theorem wopprc
Step | Hyp | Ref
| Expression |
1 | | dfsn2 4138 |
. . . . . . . . 9
⊢ {∅}
= {∅, ∅} |
2 | | id 22 |
. . . . . . . . 9
⊢
({∅} = {{𝐴},
∅} → {∅} = {{𝐴}, ∅}) |
3 | 1, 2 | syl5reqr 2659 |
. . . . . . . 8
⊢
({∅} = {{𝐴},
∅} → {{𝐴},
∅} = {∅, ∅}) |
4 | | snex 4835 |
. . . . . . . . 9
⊢ {𝐴} ∈ V |
5 | | 0ex 4718 |
. . . . . . . . 9
⊢ ∅
∈ V |
6 | 4, 5 | preqr1 4319 |
. . . . . . . 8
⊢ ({{𝐴}, ∅} = {∅, ∅}
→ {𝐴} =
∅) |
7 | 3, 6 | syl 17 |
. . . . . . 7
⊢
({∅} = {{𝐴},
∅} → {𝐴} =
∅) |
8 | | snprc 4197 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
9 | 7, 8 | sylibr 223 |
. . . . . 6
⊢
({∅} = {{𝐴},
∅} → ¬ 𝐴
∈ V) |
10 | 8 | biimpi 205 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V → {𝐴} = ∅) |
11 | 10 | preq1d 4218 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → {{𝐴}, ∅} = {∅,
∅}) |
12 | 11, 1 | syl6reqr 2663 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → {∅}
= {{𝐴},
∅}) |
13 | 9, 12 | impbii 198 |
. . . . 5
⊢
({∅} = {{𝐴},
∅} ↔ ¬ 𝐴
∈ V) |
14 | 13 | con2bii 346 |
. . . 4
⊢ (𝐴 ∈ V ↔ ¬ {∅}
= {{𝐴},
∅}) |
15 | | snprc 4197 |
. . . . . . 7
⊢ (¬
𝐵 ∈ V ↔ {𝐵} = ∅) |
16 | | eqcom 2617 |
. . . . . . 7
⊢ ({𝐵} = ∅ ↔ ∅ =
{𝐵}) |
17 | 15, 16 | bitr2i 264 |
. . . . . 6
⊢ (∅
= {𝐵} ↔ ¬ 𝐵 ∈ V) |
18 | 17 | con2bii 346 |
. . . . 5
⊢ (𝐵 ∈ V ↔ ¬ ∅ =
{𝐵}) |
19 | 5 | sneqr 4311 |
. . . . . 6
⊢
({∅} = {{𝐵}}
→ ∅ = {𝐵}) |
20 | | sneq 4135 |
. . . . . 6
⊢ (∅
= {𝐵} → {∅} =
{{𝐵}}) |
21 | 19, 20 | impbii 198 |
. . . . 5
⊢
({∅} = {{𝐵}}
↔ ∅ = {𝐵}) |
22 | 18, 21 | xchbinxr 324 |
. . . 4
⊢ (𝐵 ∈ V ↔ ¬ {∅}
= {{𝐵}}) |
23 | 14, 22 | anbi12i 729 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}})) |
24 | | pm4.56 515 |
. . . 4
⊢ ((¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}}) ↔ ¬ ({∅} = {{𝐴}, ∅} ∨ {∅} =
{{𝐵}})) |
25 | | snex 4835 |
. . . . 5
⊢ {∅}
∈ V |
26 | 25 | elpr 4146 |
. . . 4
⊢
({∅} ∈ {{{𝐴}, ∅}, {{𝐵}}} ↔ ({∅} = {{𝐴}, ∅} ∨ {∅} = {{𝐵}})) |
27 | 24, 26 | xchbinxr 324 |
. . 3
⊢ ((¬
{∅} = {{𝐴}, ∅}
∧ ¬ {∅} = {{𝐵}}) ↔ ¬ {∅} ∈ {{{𝐴}, ∅}, {{𝐵}}}) |
28 | 23, 27 | bitri 263 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬
{∅} ∈ {{{𝐴},
∅}, {{𝐵}}}) |
29 | | df1o2 7459 |
. . 3
⊢
1𝑜 = {∅} |
30 | 29 | eleq1i 2679 |
. 2
⊢
(1𝑜 ∈ {{{𝐴}, ∅}, {{𝐵}}} ↔ {∅} ∈ {{{𝐴}, ∅}, {{𝐵}}}) |
31 | 28, 30 | xchbinxr 324 |
1
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬
1𝑜 ∈ {{{𝐴}, ∅}, {{𝐵}}}) |