Step | Hyp | Ref
| Expression |
1 | | 1n0 8151 |
. . . . . . . 8
⊢
1o ≠ ∅ |
2 | 1 | neii 2936 |
. . . . . . 7
⊢ ¬
1o = ∅ |
3 | | eqtr2 2759 |
. . . . . . 7
⊢ ((𝑥 = 1o ∧ 𝑥 = ∅) → 1o
= ∅) |
4 | 2, 3 | mto 200 |
. . . . . 6
⊢ ¬
(𝑥 = 1o ∧
𝑥 =
∅) |
5 | | 1on 8139 |
. . . . . . . . 9
⊢
1o ∈ On |
6 | | 0elon 6226 |
. . . . . . . . 9
⊢ ∅
∈ On |
7 | | df-2o 8133 |
. . . . . . . . . . 11
⊢
2o = suc 1o |
8 | | df-1o 8132 |
. . . . . . . . . . 11
⊢
1o = suc ∅ |
9 | 7, 8 | eqeq12i 2753 |
. . . . . . . . . 10
⊢
(2o = 1o ↔ suc 1o = suc
∅) |
10 | | suc11 6276 |
. . . . . . . . . 10
⊢
((1o ∈ On ∧ ∅ ∈ On) → (suc
1o = suc ∅ ↔ 1o = ∅)) |
11 | 9, 10 | syl5bb 286 |
. . . . . . . . 9
⊢
((1o ∈ On ∧ ∅ ∈ On) → (2o
= 1o ↔ 1o = ∅)) |
12 | 5, 6, 11 | mp2an 692 |
. . . . . . . 8
⊢
(2o = 1o ↔ 1o =
∅) |
13 | 1, 12 | nemtbir 3029 |
. . . . . . 7
⊢ ¬
2o = 1o |
14 | | eqtr2 2759 |
. . . . . . . 8
⊢ ((𝑥 = 2o ∧ 𝑥 = 1o) →
2o = 1o) |
15 | 14 | ancoms 462 |
. . . . . . 7
⊢ ((𝑥 = 1o ∧ 𝑥 = 2o) →
2o = 1o) |
16 | 13, 15 | mto 200 |
. . . . . 6
⊢ ¬
(𝑥 = 1o ∧
𝑥 =
2o) |
17 | | nsuceq0 6253 |
. . . . . . . 8
⊢ suc
1o ≠ ∅ |
18 | 7 | eqeq1i 2743 |
. . . . . . . 8
⊢
(2o = ∅ ↔ suc 1o =
∅) |
19 | 17, 18 | nemtbir 3029 |
. . . . . . 7
⊢ ¬
2o = ∅ |
20 | | eqtr2 2759 |
. . . . . . . 8
⊢ ((𝑥 = 2o ∧ 𝑥 = ∅) → 2o
= ∅) |
21 | 20 | ancoms 462 |
. . . . . . 7
⊢ ((𝑥 = ∅ ∧ 𝑥 = 2o) →
2o = ∅) |
22 | 19, 21 | mto 200 |
. . . . . 6
⊢ ¬
(𝑥 = ∅ ∧ 𝑥 =
2o) |
23 | 4, 16, 22 | 3pm3.2ni 33229 |
. . . . 5
⊢ ¬
((𝑥 = 1o ∧
𝑥 = ∅) ∨ (𝑥 = 1o ∧ 𝑥 = 2o) ∨ (𝑥 = ∅ ∧ 𝑥 =
2o)) |
24 | | vex 3402 |
. . . . . 6
⊢ 𝑥 ∈ V |
25 | 24, 24 | brtp 33288 |
. . . . 5
⊢ (𝑥{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑥
↔ ((𝑥 = 1o
∧ 𝑥 = ∅) ∨
(𝑥 = 1o ∧
𝑥 = 2o) ∨
(𝑥 = ∅ ∧ 𝑥 =
2o))) |
26 | 23, 25 | mtbir 326 |
. . . 4
⊢ ¬
𝑥{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑥 |
27 | 26 | a1i 11 |
. . 3
⊢ (𝑥 ∈ {1o,
2o, ∅} → ¬ 𝑥{〈1o, ∅〉,
〈1o, 2o〉, 〈∅,
2o〉}𝑥) |
28 | | vex 3402 |
. . . . . . 7
⊢ 𝑦 ∈ V |
29 | 24, 28 | brtp 33288 |
. . . . . 6
⊢ (𝑥{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑦
↔ ((𝑥 = 1o
∧ 𝑦 = ∅) ∨
(𝑥 = 1o ∧
𝑦 = 2o) ∨
(𝑥 = ∅ ∧ 𝑦 =
2o))) |
30 | | vex 3402 |
. . . . . . 7
⊢ 𝑧 ∈ V |
31 | 28, 30 | brtp 33288 |
. . . . . 6
⊢ (𝑦{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑧
↔ ((𝑦 = 1o
∧ 𝑧 = ∅) ∨
(𝑦 = 1o ∧
𝑧 = 2o) ∨
(𝑦 = ∅ ∧ 𝑧 =
2o))) |
32 | | eqtr2 2759 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 1o ∧ 𝑦 = ∅) → 1o
= ∅) |
33 | 2, 32 | mto 200 |
. . . . . . . . . . . 12
⊢ ¬
(𝑦 = 1o ∧
𝑦 =
∅) |
34 | 33 | pm2.21i 119 |
. . . . . . . . . . 11
⊢ ((𝑦 = 1o ∧ 𝑦 = ∅) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
35 | 34 | ad2ant2rl 749 |
. . . . . . . . . 10
⊢ (((𝑦 = 1o ∧ 𝑧 = ∅) ∧ (𝑥 = 1o ∧ 𝑦 = ∅)) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
36 | 35 | expcom 417 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = ∅) → ((𝑦 = 1o ∧ 𝑧 = ∅) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
37 | 34 | ad2ant2rl 749 |
. . . . . . . . . 10
⊢ (((𝑦 = 1o ∧ 𝑧 = 2o) ∧ (𝑥 = 1o ∧ 𝑦 = ∅)) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
38 | 37 | expcom 417 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = ∅) → ((𝑦 = 1o ∧ 𝑧 = 2o) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
39 | | 3mix2 1332 |
. . . . . . . . . . 11
⊢ ((𝑥 = 1o ∧ 𝑧 = 2o) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
40 | 39 | ad2ant2rl 749 |
. . . . . . . . . 10
⊢ (((𝑥 = 1o ∧ 𝑦 = ∅) ∧ (𝑦 = ∅ ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
41 | 40 | ex 416 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = ∅) → ((𝑦 = ∅ ∧ 𝑧 = 2o) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
42 | 36, 38, 41 | 3jaod 1429 |
. . . . . . . 8
⊢ ((𝑥 = 1o ∧ 𝑦 = ∅) → (((𝑦 = 1o ∧ 𝑧 = ∅) ∨ (𝑦 = 1o ∧ 𝑧 = 2o) ∨ (𝑦 = ∅ ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
43 | | eqtr2 2759 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 2o ∧ 𝑦 = 1o) →
2o = 1o) |
44 | 13, 43 | mto 200 |
. . . . . . . . . . . 12
⊢ ¬
(𝑦 = 2o ∧
𝑦 =
1o) |
45 | 44 | pm2.21i 119 |
. . . . . . . . . . 11
⊢ ((𝑦 = 2o ∧ 𝑦 = 1o) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
46 | 45 | ad2ant2lr 748 |
. . . . . . . . . 10
⊢ (((𝑥 = 1o ∧ 𝑦 = 2o) ∧ (𝑦 = 1o ∧ 𝑧 = ∅)) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
47 | 46 | ex 416 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = 2o) → ((𝑦 = 1o ∧ 𝑧 = ∅) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
48 | 45 | ad2ant2lr 748 |
. . . . . . . . . 10
⊢ (((𝑥 = 1o ∧ 𝑦 = 2o) ∧ (𝑦 = 1o ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
49 | 48 | ex 416 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = 2o) → ((𝑦 = 1o ∧ 𝑧 = 2o) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
50 | | eqtr2 2759 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 2o ∧ 𝑦 = ∅) → 2o
= ∅) |
51 | 19, 50 | mto 200 |
. . . . . . . . . . . 12
⊢ ¬
(𝑦 = 2o ∧
𝑦 =
∅) |
52 | 51 | pm2.21i 119 |
. . . . . . . . . . 11
⊢ ((𝑦 = 2o ∧ 𝑦 = ∅) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
53 | 52 | ad2ant2lr 748 |
. . . . . . . . . 10
⊢ (((𝑥 = 1o ∧ 𝑦 = 2o) ∧ (𝑦 = ∅ ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
54 | 53 | ex 416 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = 2o) → ((𝑦 = ∅ ∧ 𝑧 = 2o) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
55 | 47, 49, 54 | 3jaod 1429 |
. . . . . . . 8
⊢ ((𝑥 = 1o ∧ 𝑦 = 2o) →
(((𝑦 = 1o ∧
𝑧 = ∅) ∨ (𝑦 = 1o ∧ 𝑧 = 2o) ∨ (𝑦 = ∅ ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
56 | 45 | ad2ant2lr 748 |
. . . . . . . . . 10
⊢ (((𝑥 = ∅ ∧ 𝑦 = 2o) ∧ (𝑦 = 1o ∧ 𝑧 = ∅)) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
57 | 56 | ex 416 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2o) → ((𝑦 = 1o ∧ 𝑧 = ∅) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
58 | 45 | ad2ant2lr 748 |
. . . . . . . . . 10
⊢ (((𝑥 = ∅ ∧ 𝑦 = 2o) ∧ (𝑦 = 1o ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
59 | 58 | ex 416 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2o) → ((𝑦 = 1o ∧ 𝑧 = 2o) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
60 | 52 | ad2ant2lr 748 |
. . . . . . . . . 10
⊢ (((𝑥 = ∅ ∧ 𝑦 = 2o) ∧ (𝑦 = ∅ ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
61 | 60 | ex 416 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2o) → ((𝑦 = ∅ ∧ 𝑧 = 2o) → ((𝑥 = 1o ∧ 𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
62 | 57, 59, 61 | 3jaod 1429 |
. . . . . . . 8
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2o) →
(((𝑦 = 1o ∧
𝑧 = ∅) ∨ (𝑦 = 1o ∧ 𝑧 = 2o) ∨ (𝑦 = ∅ ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
63 | 42, 55, 62 | 3jaoi 1428 |
. . . . . . 7
⊢ (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) →
(((𝑦 = 1o ∧
𝑧 = ∅) ∨ (𝑦 = 1o ∧ 𝑧 = 2o) ∨ (𝑦 = ∅ ∧ 𝑧 = 2o)) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o)))) |
64 | 63 | imp 410 |
. . . . . 6
⊢ ((((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∧ ((𝑦 = 1o ∧ 𝑧 = ∅) ∨ (𝑦 = 1o ∧ 𝑧 = 2o) ∨ (𝑦 = ∅ ∧ 𝑧 = 2o))) →
((𝑥 = 1o ∧
𝑧 = ∅) ∨ (𝑥 = 1o ∧ 𝑧 = 2o) ∨ (𝑥 = ∅ ∧ 𝑧 =
2o))) |
65 | 29, 31, 64 | syl2anb 601 |
. . . . 5
⊢ ((𝑥{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑦 ∧
𝑦{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑧)
→ ((𝑥 = 1o
∧ 𝑧 = ∅) ∨
(𝑥 = 1o ∧
𝑧 = 2o) ∨
(𝑥 = ∅ ∧ 𝑧 =
2o))) |
66 | 24, 30 | brtp 33288 |
. . . . 5
⊢ (𝑥{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑧
↔ ((𝑥 = 1o
∧ 𝑧 = ∅) ∨
(𝑥 = 1o ∧
𝑧 = 2o) ∨
(𝑥 = ∅ ∧ 𝑧 =
2o))) |
67 | 65, 66 | sylibr 237 |
. . . 4
⊢ ((𝑥{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑦 ∧
𝑦{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑧)
→ 𝑥{〈1o, ∅〉,
〈1o, 2o〉, 〈∅,
2o〉}𝑧) |
68 | 67 | a1i 11 |
. . 3
⊢ ((𝑥 ∈ {1o,
2o, ∅} ∧ 𝑦 ∈ {1o, 2o,
∅} ∧ 𝑧 ∈
{1o, 2o, ∅}) → ((𝑥{〈1o, ∅〉,
〈1o, 2o〉, 〈∅,
2o〉}𝑦 ∧
𝑦{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑧)
→ 𝑥{〈1o, ∅〉,
〈1o, 2o〉, 〈∅,
2o〉}𝑧)) |
69 | 24 | eltp 4580 |
. . . . 5
⊢ (𝑥 ∈ {1o,
2o, ∅} ↔ (𝑥 = 1o ∨ 𝑥 = 2o ∨ 𝑥 = ∅)) |
70 | 28 | eltp 4580 |
. . . . 5
⊢ (𝑦 ∈ {1o,
2o, ∅} ↔ (𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅)) |
71 | | eqtr3 2760 |
. . . . . . . . . 10
⊢ ((𝑥 = 1o ∧ 𝑦 = 1o) → 𝑥 = 𝑦) |
72 | 71 | 3mix2d 1338 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = 1o) →
(((𝑥 = 1o ∧
𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
73 | 72 | ex 416 |
. . . . . . . 8
⊢ (𝑥 = 1o → (𝑦 = 1o → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
74 | | 3mix2 1332 |
. . . . . . . . . 10
⊢ ((𝑥 = 1o ∧ 𝑦 = 2o) → ((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 =
2o))) |
75 | 74 | 3mix1d 1337 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = 2o) →
(((𝑥 = 1o ∧
𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
76 | 75 | ex 416 |
. . . . . . . 8
⊢ (𝑥 = 1o → (𝑦 = 2o → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
77 | | 3mix1 1331 |
. . . . . . . . . 10
⊢ ((𝑥 = 1o ∧ 𝑦 = ∅) → ((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 =
2o))) |
78 | 77 | 3mix1d 1337 |
. . . . . . . . 9
⊢ ((𝑥 = 1o ∧ 𝑦 = ∅) → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
79 | 78 | ex 416 |
. . . . . . . 8
⊢ (𝑥 = 1o → (𝑦 = ∅ → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
80 | 73, 76, 79 | 3jaod 1429 |
. . . . . . 7
⊢ (𝑥 = 1o → ((𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅) → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
81 | | 3mix2 1332 |
. . . . . . . . . 10
⊢ ((𝑦 = 1o ∧ 𝑥 = 2o) → ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 =
2o))) |
82 | 81 | 3mix3d 1339 |
. . . . . . . . 9
⊢ ((𝑦 = 1o ∧ 𝑥 = 2o) →
(((𝑥 = 1o ∧
𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
83 | 82 | expcom 417 |
. . . . . . . 8
⊢ (𝑥 = 2o → (𝑦 = 1o → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
84 | | eqtr3 2760 |
. . . . . . . . . 10
⊢ ((𝑥 = 2o ∧ 𝑦 = 2o) → 𝑥 = 𝑦) |
85 | 84 | 3mix2d 1338 |
. . . . . . . . 9
⊢ ((𝑥 = 2o ∧ 𝑦 = 2o) →
(((𝑥 = 1o ∧
𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
86 | 85 | ex 416 |
. . . . . . . 8
⊢ (𝑥 = 2o → (𝑦 = 2o → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
87 | | 3mix3 1333 |
. . . . . . . . . 10
⊢ ((𝑦 = ∅ ∧ 𝑥 = 2o) → ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 =
2o))) |
88 | 87 | 3mix3d 1339 |
. . . . . . . . 9
⊢ ((𝑦 = ∅ ∧ 𝑥 = 2o) →
(((𝑥 = 1o ∧
𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
89 | 88 | expcom 417 |
. . . . . . . 8
⊢ (𝑥 = 2o → (𝑦 = ∅ → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
90 | 83, 86, 89 | 3jaod 1429 |
. . . . . . 7
⊢ (𝑥 = 2o → ((𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅) → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
91 | | 3mix1 1331 |
. . . . . . . . . 10
⊢ ((𝑦 = 1o ∧ 𝑥 = ∅) → ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 =
2o))) |
92 | 91 | 3mix3d 1339 |
. . . . . . . . 9
⊢ ((𝑦 = 1o ∧ 𝑥 = ∅) → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
93 | 92 | expcom 417 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑦 = 1o → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
94 | | 3mix3 1333 |
. . . . . . . . . 10
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2o) → ((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 =
2o))) |
95 | 94 | 3mix1d 1337 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = 2o) →
(((𝑥 = 1o ∧
𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
96 | 95 | ex 416 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑦 = 2o → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
97 | | eqtr3 2760 |
. . . . . . . . . 10
⊢ ((𝑥 = ∅ ∧ 𝑦 = ∅) → 𝑥 = 𝑦) |
98 | 97 | 3mix2d 1338 |
. . . . . . . . 9
⊢ ((𝑥 = ∅ ∧ 𝑦 = ∅) → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
99 | 98 | ex 416 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑦 = ∅ → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
100 | 93, 96, 99 | 3jaod 1429 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅) → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
101 | 80, 90, 100 | 3jaoi 1428 |
. . . . . 6
⊢ ((𝑥 = 1o ∨ 𝑥 = 2o ∨ 𝑥 = ∅) → ((𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅) → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o))))) |
102 | 101 | imp 410 |
. . . . 5
⊢ (((𝑥 = 1o ∨ 𝑥 = 2o ∨ 𝑥 = ∅) ∧ (𝑦 = 1o ∨ 𝑦 = 2o ∨ 𝑦 = ∅)) → (((𝑥 = 1o ∧ 𝑦 = ∅) ∨ (𝑥 = 1o ∧ 𝑦 = 2o) ∨ (𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
103 | 69, 70, 102 | syl2anb 601 |
. . . 4
⊢ ((𝑥 ∈ {1o,
2o, ∅} ∧ 𝑦 ∈ {1o, 2o,
∅}) → (((𝑥 =
1o ∧ 𝑦 =
∅) ∨ (𝑥 =
1o ∧ 𝑦 =
2o) ∨ (𝑥 =
∅ ∧ 𝑦 =
2o)) ∨ 𝑥 =
𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
104 | | biid 264 |
. . . . 5
⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦) |
105 | 28, 24 | brtp 33288 |
. . . . 5
⊢ (𝑦{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑥
↔ ((𝑦 = 1o
∧ 𝑥 = ∅) ∨
(𝑦 = 1o ∧
𝑥 = 2o) ∨
(𝑦 = ∅ ∧ 𝑥 =
2o))) |
106 | 29, 104, 105 | 3orbi123i 1157 |
. . . 4
⊢ ((𝑥{〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉}𝑦 ∨
𝑥 = 𝑦 ∨ 𝑦{〈1o, ∅〉,
〈1o, 2o〉, 〈∅,
2o〉}𝑥)
↔ (((𝑥 = 1o
∧ 𝑦 = ∅) ∨
(𝑥 = 1o ∧
𝑦 = 2o) ∨
(𝑥 = ∅ ∧ 𝑦 = 2o)) ∨ 𝑥 = 𝑦 ∨ ((𝑦 = 1o ∧ 𝑥 = ∅) ∨ (𝑦 = 1o ∧ 𝑥 = 2o) ∨ (𝑦 = ∅ ∧ 𝑥 = 2o)))) |
107 | 103, 106 | sylibr 237 |
. . 3
⊢ ((𝑥 ∈ {1o,
2o, ∅} ∧ 𝑦 ∈ {1o, 2o,
∅}) → (𝑥{〈1o, ∅〉,
〈1o, 2o〉, 〈∅,
2o〉}𝑦 ∨
𝑥 = 𝑦 ∨ 𝑦{〈1o, ∅〉,
〈1o, 2o〉, 〈∅,
2o〉}𝑥)) |
108 | 27, 68, 107 | issoi 5477 |
. 2
⊢
{〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉} Or {1o,
2o, ∅} |
109 | | df-tp 4522 |
. . 3
⊢
{1o, 2o, ∅} = ({1o,
2o} ∪ {∅}) |
110 | | soeq2 5465 |
. . 3
⊢
({1o, 2o, ∅} = ({1o,
2o} ∪ {∅}) → ({〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
Or {1o, 2o, ∅} ↔ {〈1o,
∅〉, 〈1o, 2o〉, 〈∅,
2o〉} Or ({1o, 2o} ∪
{∅}))) |
111 | 109, 110 | ax-mp 5 |
. 2
⊢
({〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉} Or {1o,
2o, ∅} ↔ {〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
Or ({1o, 2o} ∪ {∅})) |
112 | 108, 111 | mpbi 233 |
1
⊢
{〈1o, ∅〉, 〈1o,
2o〉, 〈∅, 2o〉} Or ({1o,
2o} ∪ {∅}) |