Step | Hyp | Ref
| Expression |
1 | | 1n0 7462 |
. . . . . . . 8
⊢
1𝑜 ≠ ∅ |
2 | 1 | neii 2784 |
. . . . . . 7
⊢ ¬
1𝑜 = ∅ |
3 | | eqtr2 2630 |
. . . . . . 7
⊢ ((𝑥 = 1𝑜 ∧
𝑥 = ∅) →
1𝑜 = ∅) |
4 | 2, 3 | mto 187 |
. . . . . 6
⊢ ¬
(𝑥 = 1𝑜
∧ 𝑥 =
∅) |
5 | | 1on 7454 |
. . . . . . . . 9
⊢
1𝑜 ∈ On |
6 | | 0elon 5695 |
. . . . . . . . 9
⊢ ∅
∈ On |
7 | | df-2o 7448 |
. . . . . . . . . . 11
⊢
2𝑜 = suc 1𝑜 |
8 | | df-1o 7447 |
. . . . . . . . . . 11
⊢
1𝑜 = suc ∅ |
9 | 7, 8 | eqeq12i 2624 |
. . . . . . . . . 10
⊢
(2𝑜 = 1𝑜 ↔ suc
1𝑜 = suc ∅) |
10 | | suc11 5748 |
. . . . . . . . . 10
⊢
((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc
1𝑜 = suc ∅ ↔ 1𝑜 =
∅)) |
11 | 9, 10 | syl5bb 271 |
. . . . . . . . 9
⊢
((1𝑜 ∈ On ∧ ∅ ∈ On) →
(2𝑜 = 1𝑜 ↔ 1𝑜 =
∅)) |
12 | 5, 6, 11 | mp2an 704 |
. . . . . . . 8
⊢
(2𝑜 = 1𝑜 ↔
1𝑜 = ∅) |
13 | 1, 12 | nemtbir 2877 |
. . . . . . 7
⊢ ¬
2𝑜 = 1𝑜 |
14 | | eqtr2 2630 |
. . . . . . . 8
⊢ ((𝑥 = 2𝑜 ∧
𝑥 = 1𝑜)
→ 2𝑜 = 1𝑜) |
15 | 14 | ancoms 468 |
. . . . . . 7
⊢ ((𝑥 = 1𝑜 ∧
𝑥 = 2𝑜)
→ 2𝑜 = 1𝑜) |
16 | 13, 15 | mto 187 |
. . . . . 6
⊢ ¬
(𝑥 = 1𝑜
∧ 𝑥 =
2𝑜) |
17 | | nsuceq0 5722 |
. . . . . . . 8
⊢ suc
1𝑜 ≠ ∅ |
18 | 7 | eqeq1i 2615 |
. . . . . . . 8
⊢
(2𝑜 = ∅ ↔ suc 1𝑜 =
∅) |
19 | 17, 18 | nemtbir 2877 |
. . . . . . 7
⊢ ¬
2𝑜 = ∅ |
20 | | eqtr2 2630 |
. . . . . . . 8
⊢ ((𝑥 = 2𝑜 ∧
𝑥 = ∅) →
2𝑜 = ∅) |
21 | 20 | ancoms 468 |
. . . . . . 7
⊢ ((𝑥 = ∅ ∧ 𝑥 = 2𝑜) →
2𝑜 = ∅) |
22 | 19, 21 | mto 187 |
. . . . . 6
⊢ ¬
(𝑥 = ∅ ∧ 𝑥 =
2𝑜) |
23 | 4, 16, 22 | 3pm3.2ni 30849 |
. . . . 5
⊢ ¬
((𝑥 = 1𝑜
∧ 𝑥 = ∅) ∨
(𝑥 = 1𝑜
∧ 𝑥 =
2𝑜) ∨ (𝑥 = ∅ ∧ 𝑥 = 2𝑜)) |
24 | | vex 3176 |
. . . . . 6
⊢ 𝑥 ∈ V |
25 | 24, 24 | brtp 30892 |
. . . . 5
⊢ (𝑥{〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}𝑥 ↔ ((𝑥 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑥 =
2𝑜))) |
26 | 23, 25 | mtbir 312 |
. . . 4
⊢ ¬
𝑥{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑥 |
27 | 26 | a1i 11 |
. . 3
⊢ (𝑥 ∈ {1𝑜,
2𝑜, ∅} → ¬ 𝑥{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑥) |
28 | | vex 3176 |
. . . . . . 7
⊢ 𝑦 ∈ V |
29 | 24, 28 | brtp 30892 |
. . . . . 6
⊢ (𝑥{〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}𝑦 ↔ ((𝑥 = 1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 =
2𝑜))) |
30 | | vex 3176 |
. . . . . . 7
⊢ 𝑧 ∈ V |
31 | 28, 30 | brtp 30892 |
. . . . . 6
⊢ (𝑦{〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}𝑧 ↔ ((𝑦 = 1𝑜 ∧ 𝑧 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑧 =
2𝑜))) |
32 | | eqtr2 2630 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 1𝑜 ∧
𝑦 = ∅) →
1𝑜 = ∅) |
33 | 2, 32 | mto 187 |
. . . . . . . . . . . 12
⊢ ¬
(𝑦 = 1𝑜
∧ 𝑦 =
∅) |
34 | 33 | pm2.21i 115 |
. . . . . . . . . . 11
⊢ ((𝑦 = 1𝑜 ∧
𝑦 = ∅) → ((𝑥 = 1𝑜 ∧
𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜))) |
35 | 34 | ad2ant2rl 781 |
. . . . . . . . . 10
⊢ (((𝑦 = 1𝑜 ∧
𝑧 = ∅) ∧ (𝑥 = 1𝑜 ∧
𝑦 = ∅)) →
((𝑥 = 1𝑜
∧ 𝑧 = ∅) ∨
(𝑥 = 1𝑜
∧ 𝑧 =
2𝑜) ∨ (𝑥 = ∅ ∧ 𝑧 = 2𝑜))) |
36 | 35 | expcom 450 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = ∅) → ((𝑦 = 1𝑜 ∧
𝑧 = ∅) → ((𝑥 = 1𝑜 ∧
𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜)))) |
37 | 34 | ad2ant2rl 781 |
. . . . . . . . . 10
⊢ (((𝑦 = 1𝑜 ∧
𝑧 = 2𝑜)
∧ (𝑥 =
1𝑜 ∧ 𝑦 = ∅)) → ((𝑥 = 1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜))) |
38 | 37 | expcom 450 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = ∅) → ((𝑦 = 1𝑜 ∧
𝑧 = 2𝑜)
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜)))) |
39 | | 3mix2 1224 |
. . . . . . . . . . 11
⊢ ((𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜))) |
40 | 39 | ad2ant2rl 781 |
. . . . . . . . . 10
⊢ (((𝑥 = 1𝑜 ∧
𝑦 = ∅) ∧ (𝑦 = ∅ ∧ 𝑧 = 2𝑜))
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜))) |
41 | 40 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = ∅) → ((𝑦 = ∅ ∧ 𝑧 = 2𝑜) →
((𝑥 = 1𝑜
∧ 𝑧 = ∅) ∨
(𝑥 = 1𝑜
∧ 𝑧 =
2𝑜) ∨ (𝑥 = ∅ ∧ 𝑧 = 2𝑜)))) |
42 | 36, 38, 41 | 3jaod 1384 |
. . . . . . . 8
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = ∅) →
(((𝑦 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑦 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑦 = ∅ ∧ 𝑧 = 2𝑜))
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜)))) |
43 | | eqtr2 2630 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 2𝑜 ∧
𝑦 = 1𝑜)
→ 2𝑜 = 1𝑜) |
44 | 13, 43 | mto 187 |
. . . . . . . . . . . 12
⊢ ¬
(𝑦 = 2𝑜
∧ 𝑦 =
1𝑜) |
45 | 44 | pm2.21i 115 |
. . . . . . . . . . 11
⊢ ((𝑦 = 2𝑜 ∧
𝑦 = 1𝑜)
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜))) |
46 | 45 | ad2ant2lr 780 |
. . . . . . . . . 10
⊢ (((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∧ (𝑦 =
1𝑜 ∧ 𝑧 = ∅)) → ((𝑥 = 1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜))) |
47 | 46 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
→ ((𝑦 =
1𝑜 ∧ 𝑧 = ∅) → ((𝑥 = 1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜)))) |
48 | 45 | ad2ant2lr 780 |
. . . . . . . . . 10
⊢ (((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∧ (𝑦 =
1𝑜 ∧ 𝑧 = 2𝑜)) → ((𝑥 = 1𝑜 ∧
𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜))) |
49 | 48 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
→ ((𝑦 =
1𝑜 ∧ 𝑧 = 2𝑜) → ((𝑥 = 1𝑜 ∧
𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜)))) |
50 | | eqtr2 2630 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 2𝑜 ∧
𝑦 = ∅) →
2𝑜 = ∅) |
51 | 19, 50 | mto 187 |
. . . . . . . . . . . 12
⊢ ¬
(𝑦 = 2𝑜
∧ 𝑦 =
∅) |
52 | 51 | pm2.21i 115 |
. . . . . . . . . . 11
⊢ ((𝑦 = 2𝑜 ∧
𝑦 = ∅) → ((𝑥 = 1𝑜 ∧
𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜))) |
53 | 52 | ad2ant2lr 780 |
. . . . . . . . . 10
⊢ (((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∧ (𝑦 = ∅ ∧
𝑧 = 2𝑜))
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜))) |
54 | 53 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
→ ((𝑦 = ∅ ∧
𝑧 = 2𝑜)
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜)))) |
55 | 47, 49, 54 | 3jaod 1384 |
. . . . . . . 8
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
→ (((𝑦 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑦 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑦 = ∅ ∧ 𝑧 = 2𝑜))
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜)))) |
56 | 45 | ad2ant2lr 780 |
. . . . . . . . . 10
⊢ (((𝑥 = ∅ ∧ 𝑦 = 2𝑜) ∧
(𝑦 = 1𝑜
∧ 𝑧 = ∅)) →
((𝑥 = 1𝑜
∧ 𝑧 = ∅) ∨
(𝑥 = 1𝑜
∧ 𝑧 =
2𝑜) ∨ (𝑥 = ∅ ∧ 𝑧 = 2𝑜))) |
57 | 56 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2𝑜) →
((𝑦 = 1𝑜
∧ 𝑧 = ∅) →
((𝑥 = 1𝑜
∧ 𝑧 = ∅) ∨
(𝑥 = 1𝑜
∧ 𝑧 =
2𝑜) ∨ (𝑥 = ∅ ∧ 𝑧 = 2𝑜)))) |
58 | 45 | ad2ant2lr 780 |
. . . . . . . . . 10
⊢ (((𝑥 = ∅ ∧ 𝑦 = 2𝑜) ∧
(𝑦 = 1𝑜
∧ 𝑧 =
2𝑜)) → ((𝑥 = 1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜))) |
59 | 58 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2𝑜) →
((𝑦 = 1𝑜
∧ 𝑧 =
2𝑜) → ((𝑥 = 1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜)))) |
60 | 52 | ad2ant2lr 780 |
. . . . . . . . . 10
⊢ (((𝑥 = ∅ ∧ 𝑦 = 2𝑜) ∧
(𝑦 = ∅ ∧ 𝑧 = 2𝑜))
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜))) |
61 | 60 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2𝑜) →
((𝑦 = ∅ ∧ 𝑧 = 2𝑜) →
((𝑥 = 1𝑜
∧ 𝑧 = ∅) ∨
(𝑥 = 1𝑜
∧ 𝑧 =
2𝑜) ∨ (𝑥 = ∅ ∧ 𝑧 = 2𝑜)))) |
62 | 57, 59, 61 | 3jaod 1384 |
. . . . . . . 8
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2𝑜) →
(((𝑦 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑦 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑦 = ∅ ∧ 𝑧 = 2𝑜))
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜)))) |
63 | 42, 55, 62 | 3jaoi 1383 |
. . . . . . 7
⊢ (((𝑥 = 1𝑜 ∧
𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
→ (((𝑦 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑦 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑦 = ∅ ∧ 𝑧 = 2𝑜))
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜)))) |
64 | 63 | imp 444 |
. . . . . 6
⊢ ((((𝑥 = 1𝑜 ∧
𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∧ ((𝑦 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑦 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑦 = ∅ ∧ 𝑧 = 2𝑜)))
→ ((𝑥 =
1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑧 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑧 =
2𝑜))) |
65 | 29, 31, 64 | syl2anb 495 |
. . . . 5
⊢ ((𝑥{〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}𝑦 ∧ 𝑦{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑧) → ((𝑥 = 1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜))) |
66 | 24, 30 | brtp 30892 |
. . . . 5
⊢ (𝑥{〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}𝑧 ↔ ((𝑥 = 1𝑜 ∧ 𝑧 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑧 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑧 =
2𝑜))) |
67 | 65, 66 | sylibr 223 |
. . . 4
⊢ ((𝑥{〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}𝑦 ∧ 𝑦{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑧) → 𝑥{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑧) |
68 | 67 | a1i 11 |
. . 3
⊢ ((𝑥 ∈ {1𝑜,
2𝑜, ∅} ∧ 𝑦 ∈ {1𝑜,
2𝑜, ∅} ∧ 𝑧 ∈ {1𝑜,
2𝑜, ∅}) → ((𝑥{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑦 ∧ 𝑦{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑧) → 𝑥{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑧)) |
69 | 24 | eltp 4177 |
. . . . 5
⊢ (𝑥 ∈ {1𝑜,
2𝑜, ∅} ↔ (𝑥 = 1𝑜 ∨ 𝑥 = 2𝑜 ∨
𝑥 =
∅)) |
70 | 28 | eltp 4177 |
. . . . 5
⊢ (𝑦 ∈ {1𝑜,
2𝑜, ∅} ↔ (𝑦 = 1𝑜 ∨ 𝑦 = 2𝑜 ∨
𝑦 =
∅)) |
71 | | eqtr3 2631 |
. . . . . . . . . 10
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = 1𝑜)
→ 𝑥 = 𝑦) |
72 | 71 | 3mix2d 1230 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = 1𝑜)
→ (((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
73 | 72 | ex 449 |
. . . . . . . 8
⊢ (𝑥 = 1𝑜 →
(𝑦 = 1𝑜
→ (((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
74 | | 3mix2 1224 |
. . . . . . . . . 10
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
→ ((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 =
2𝑜))) |
75 | 74 | 3mix1d 1229 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
→ (((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
76 | 75 | ex 449 |
. . . . . . . 8
⊢ (𝑥 = 1𝑜 →
(𝑦 = 2𝑜
→ (((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
77 | | 3mix1 1223 |
. . . . . . . . . 10
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = ∅) → ((𝑥 = 1𝑜 ∧
𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 =
2𝑜))) |
78 | 77 | 3mix1d 1229 |
. . . . . . . . 9
⊢ ((𝑥 = 1𝑜 ∧
𝑦 = ∅) →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
79 | 78 | ex 449 |
. . . . . . . 8
⊢ (𝑥 = 1𝑜 →
(𝑦 = ∅ →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
80 | 73, 76, 79 | 3jaod 1384 |
. . . . . . 7
⊢ (𝑥 = 1𝑜 →
((𝑦 = 1𝑜
∨ 𝑦 =
2𝑜 ∨ 𝑦 = ∅) → (((𝑥 = 1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
81 | | 3mix2 1224 |
. . . . . . . . . 10
⊢ ((𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
→ ((𝑦 =
1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧ 𝑥 = 2𝑜) ∨
(𝑦 = ∅ ∧ 𝑥 =
2𝑜))) |
82 | 81 | 3mix3d 1231 |
. . . . . . . . 9
⊢ ((𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
→ (((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
83 | 82 | expcom 450 |
. . . . . . . 8
⊢ (𝑥 = 2𝑜 →
(𝑦 = 1𝑜
→ (((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
84 | | eqtr3 2631 |
. . . . . . . . . 10
⊢ ((𝑥 = 2𝑜 ∧
𝑦 = 2𝑜)
→ 𝑥 = 𝑦) |
85 | 84 | 3mix2d 1230 |
. . . . . . . . 9
⊢ ((𝑥 = 2𝑜 ∧
𝑦 = 2𝑜)
→ (((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
86 | 85 | ex 449 |
. . . . . . . 8
⊢ (𝑥 = 2𝑜 →
(𝑦 = 2𝑜
→ (((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
87 | | 3mix3 1225 |
. . . . . . . . . 10
⊢ ((𝑦 = ∅ ∧ 𝑥 = 2𝑜) →
((𝑦 = 1𝑜
∧ 𝑥 = ∅) ∨
(𝑦 = 1𝑜
∧ 𝑥 =
2𝑜) ∨ (𝑦 = ∅ ∧ 𝑥 = 2𝑜))) |
88 | 87 | 3mix3d 1231 |
. . . . . . . . 9
⊢ ((𝑦 = ∅ ∧ 𝑥 = 2𝑜) →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
89 | 88 | expcom 450 |
. . . . . . . 8
⊢ (𝑥 = 2𝑜 →
(𝑦 = ∅ →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
90 | 83, 86, 89 | 3jaod 1384 |
. . . . . . 7
⊢ (𝑥 = 2𝑜 →
((𝑦 = 1𝑜
∨ 𝑦 =
2𝑜 ∨ 𝑦 = ∅) → (((𝑥 = 1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
91 | | 3mix1 1223 |
. . . . . . . . . 10
⊢ ((𝑦 = 1𝑜 ∧
𝑥 = ∅) → ((𝑦 = 1𝑜 ∧
𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))) |
92 | 91 | 3mix3d 1231 |
. . . . . . . . 9
⊢ ((𝑦 = 1𝑜 ∧
𝑥 = ∅) →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
93 | 92 | expcom 450 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑦 = 1𝑜 →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
94 | | 3mix3 1225 |
. . . . . . . . . 10
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2𝑜) →
((𝑥 = 1𝑜
∧ 𝑦 = ∅) ∨
(𝑥 = 1𝑜
∧ 𝑦 =
2𝑜) ∨ (𝑥 = ∅ ∧ 𝑦 = 2𝑜))) |
95 | 94 | 3mix1d 1229 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2𝑜) →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
96 | 95 | ex 449 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑦 = 2𝑜 →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
97 | | eqtr3 2631 |
. . . . . . . . . 10
⊢ ((𝑥 = ∅ ∧ 𝑦 = ∅) → 𝑥 = 𝑦) |
98 | 97 | 3mix2d 1230 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = ∅) → (((𝑥 = 1𝑜 ∧
𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
99 | 98 | ex 449 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑦 = ∅ → (((𝑥 = 1𝑜 ∧
𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
100 | 93, 96, 99 | 3jaod 1384 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑦 = 1𝑜 ∨
𝑦 = 2𝑜
∨ 𝑦 = ∅) →
(((𝑥 =
1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧ 𝑦 = 2𝑜) ∨
(𝑥 = ∅ ∧ 𝑦 = 2𝑜)) ∨
𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
101 | 80, 90, 100 | 3jaoi 1383 |
. . . . . 6
⊢ ((𝑥 = 1𝑜 ∨
𝑥 = 2𝑜
∨ 𝑥 = ∅) →
((𝑦 = 1𝑜
∨ 𝑦 =
2𝑜 ∨ 𝑦 = ∅) → (((𝑥 = 1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))))) |
102 | 101 | imp 444 |
. . . . 5
⊢ (((𝑥 = 1𝑜 ∨
𝑥 = 2𝑜
∨ 𝑥 = ∅) ∧
(𝑦 = 1𝑜
∨ 𝑦 =
2𝑜 ∨ 𝑦 = ∅)) → (((𝑥 = 1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
103 | 69, 70, 102 | syl2anb 495 |
. . . 4
⊢ ((𝑥 ∈ {1𝑜,
2𝑜, ∅} ∧ 𝑦 ∈ {1𝑜,
2𝑜, ∅}) → (((𝑥 = 1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
104 | | biid 250 |
. . . . 5
⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦) |
105 | 28, 24 | brtp 30892 |
. . . . 5
⊢ (𝑦{〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}𝑥 ↔ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜))) |
106 | 29, 104, 105 | 3orbi123i 1245 |
. . . 4
⊢ ((𝑥{〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑥) ↔ (((𝑥 = 1𝑜 ∧ 𝑦 = ∅) ∨ (𝑥 = 1𝑜 ∧
𝑦 = 2𝑜)
∨ (𝑥 = ∅ ∧
𝑦 = 2𝑜))
∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1𝑜 ∧ 𝑥 = ∅) ∨ (𝑦 = 1𝑜 ∧
𝑥 = 2𝑜)
∨ (𝑦 = ∅ ∧
𝑥 =
2𝑜)))) |
107 | 103, 106 | sylibr 223 |
. . 3
⊢ ((𝑥 ∈ {1𝑜,
2𝑜, ∅} ∧ 𝑦 ∈ {1𝑜,
2𝑜, ∅}) → (𝑥{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉}𝑥)) |
108 | 27, 68, 107 | issoi 4990 |
. 2
⊢
{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} Or {1𝑜, 2𝑜,
∅} |
109 | | df-tp 4130 |
. . 3
⊢
{1𝑜, 2𝑜, ∅} =
({1𝑜, 2𝑜} ∪
{∅}) |
110 | | soeq2 4979 |
. . 3
⊢
({1𝑜, 2𝑜, ∅} =
({1𝑜, 2𝑜} ∪ {∅}) →
({〈1𝑜, ∅〉, 〈1𝑜,
2𝑜〉, 〈∅, 2𝑜〉} Or
{1𝑜, 2𝑜, ∅} ↔
{〈1𝑜, ∅〉, 〈1𝑜,
2𝑜〉, 〈∅, 2𝑜〉} Or
({1𝑜, 2𝑜} ∪
{∅}))) |
111 | 109, 110 | ax-mp 5 |
. 2
⊢
({〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} Or {1𝑜, 2𝑜,
∅} ↔ {〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} Or ({1𝑜, 2𝑜}
∪ {∅})) |
112 | 108, 111 | mpbi 219 |
1
⊢
{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} Or ({1𝑜, 2𝑜}
∪ {∅}) |