Proof of Theorem opthwiener
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . 7
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}}) |
2 | | snex 5324 |
. . . . . . . . . . . 12
⊢ {{𝐵}} ∈ V |
3 | 2 | prid2 4679 |
. . . . . . . . . . 11
⊢ {{𝐵}} ∈ {{{𝐴}, ∅}, {{𝐵}}} |
4 | | eleq2 2826 |
. . . . . . . . . . 11
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → ({{𝐵}} ∈ {{{𝐴}, ∅}, {{𝐵}}} ↔ {{𝐵}} ∈ {{{𝐶}, ∅}, {{𝐷}}})) |
5 | 3, 4 | mpbii 236 |
. . . . . . . . . 10
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{𝐵}} ∈ {{{𝐶}, ∅}, {{𝐷}}}) |
6 | 2 | elpr 4564 |
. . . . . . . . . 10
⊢ ({{𝐵}} ∈ {{{𝐶}, ∅}, {{𝐷}}} ↔ ({{𝐵}} = {{𝐶}, ∅} ∨ {{𝐵}} = {{𝐷}})) |
7 | 5, 6 | sylib 221 |
. . . . . . . . 9
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → ({{𝐵}} = {{𝐶}, ∅} ∨ {{𝐵}} = {{𝐷}})) |
8 | | 0ex 5200 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
9 | 8 | prid2 4679 |
. . . . . . . . . . . 12
⊢ ∅
∈ {{𝐶},
∅} |
10 | | opthw.2 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈ V |
11 | 10 | snnz 4692 |
. . . . . . . . . . . . 13
⊢ {𝐵} ≠ ∅ |
12 | 8 | elsn 4556 |
. . . . . . . . . . . . . 14
⊢ (∅
∈ {{𝐵}} ↔ ∅
= {𝐵}) |
13 | | eqcom 2744 |
. . . . . . . . . . . . . 14
⊢ (∅
= {𝐵} ↔ {𝐵} = ∅) |
14 | 12, 13 | bitri 278 |
. . . . . . . . . . . . 13
⊢ (∅
∈ {{𝐵}} ↔ {𝐵} = ∅) |
15 | 11, 14 | nemtbir 3037 |
. . . . . . . . . . . 12
⊢ ¬
∅ ∈ {{𝐵}} |
16 | | nelneq2 2863 |
. . . . . . . . . . . 12
⊢ ((∅
∈ {{𝐶}, ∅} ∧
¬ ∅ ∈ {{𝐵}})
→ ¬ {{𝐶}, ∅}
= {{𝐵}}) |
17 | 9, 15, 16 | mp2an 692 |
. . . . . . . . . . 11
⊢ ¬
{{𝐶}, ∅} = {{𝐵}} |
18 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ ({{𝐶}, ∅} = {{𝐵}} ↔ {{𝐵}} = {{𝐶}, ∅}) |
19 | 17, 18 | mtbi 325 |
. . . . . . . . . 10
⊢ ¬
{{𝐵}} = {{𝐶}, ∅} |
20 | | biorf 937 |
. . . . . . . . . 10
⊢ (¬
{{𝐵}} = {{𝐶}, ∅} → ({{𝐵}} = {{𝐷}} ↔ ({{𝐵}} = {{𝐶}, ∅} ∨ {{𝐵}} = {{𝐷}}))) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . 9
⊢ ({{𝐵}} = {{𝐷}} ↔ ({{𝐵}} = {{𝐶}, ∅} ∨ {{𝐵}} = {{𝐷}})) |
22 | 7, 21 | sylibr 237 |
. . . . . . . 8
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{𝐵}} = {{𝐷}}) |
23 | 22 | preq2d 4656 |
. . . . . . 7
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{{𝐶}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}}) |
24 | 1, 23 | eqtr4d 2780 |
. . . . . 6
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐵}}}) |
25 | | prex 5325 |
. . . . . . 7
⊢ {{𝐴}, ∅} ∈
V |
26 | | prex 5325 |
. . . . . . 7
⊢ {{𝐶}, ∅} ∈
V |
27 | 25, 26 | preqr1 4759 |
. . . . . 6
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐵}}} → {{𝐴}, ∅} = {{𝐶}, ∅}) |
28 | 24, 27 | syl 17 |
. . . . 5
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {{𝐴}, ∅} = {{𝐶}, ∅}) |
29 | | snex 5324 |
. . . . . 6
⊢ {𝐴} ∈ V |
30 | | snex 5324 |
. . . . . 6
⊢ {𝐶} ∈ V |
31 | 29, 30 | preqr1 4759 |
. . . . 5
⊢ ({{𝐴}, ∅} = {{𝐶}, ∅} → {𝐴} = {𝐶}) |
32 | 28, 31 | syl 17 |
. . . 4
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {𝐴} = {𝐶}) |
33 | | opthw.1 |
. . . . 5
⊢ 𝐴 ∈ V |
34 | 33 | sneqr 4751 |
. . . 4
⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶) |
35 | 32, 34 | syl 17 |
. . 3
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → 𝐴 = 𝐶) |
36 | | snex 5324 |
. . . . . 6
⊢ {𝐵} ∈ V |
37 | 36 | sneqr 4751 |
. . . . 5
⊢ ({{𝐵}} = {{𝐷}} → {𝐵} = {𝐷}) |
38 | 22, 37 | syl 17 |
. . . 4
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → {𝐵} = {𝐷}) |
39 | 10 | sneqr 4751 |
. . . 4
⊢ ({𝐵} = {𝐷} → 𝐵 = 𝐷) |
40 | 38, 39 | syl 17 |
. . 3
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → 𝐵 = 𝐷) |
41 | 35, 40 | jca 515 |
. 2
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
42 | | sneq 4551 |
. . . . 5
⊢ (𝐴 = 𝐶 → {𝐴} = {𝐶}) |
43 | 42 | preq1d 4655 |
. . . 4
⊢ (𝐴 = 𝐶 → {{𝐴}, ∅} = {{𝐶}, ∅}) |
44 | 43 | preq1d 4655 |
. . 3
⊢ (𝐴 = 𝐶 → {{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐵}}}) |
45 | | sneq 4551 |
. . . . 5
⊢ (𝐵 = 𝐷 → {𝐵} = {𝐷}) |
46 | | sneq 4551 |
. . . . 5
⊢ ({𝐵} = {𝐷} → {{𝐵}} = {{𝐷}}) |
47 | 45, 46 | syl 17 |
. . . 4
⊢ (𝐵 = 𝐷 → {{𝐵}} = {{𝐷}}) |
48 | 47 | preq2d 4656 |
. . 3
⊢ (𝐵 = 𝐷 → {{{𝐶}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}}) |
49 | 44, 48 | sylan9eq 2798 |
. 2
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}}) |
50 | 41, 49 | impbii 212 |
1
⊢ ({{{𝐴}, ∅}, {{𝐵}}} = {{{𝐶}, ∅}, {{𝐷}}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |