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