Metamath Proof Explorer


Theorem sltsolem1

Description: Lemma for sltso . The sign expansion relationship totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011)

Ref Expression
Assertion sltsolem1 { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or ( { 1o , 2o } ∪ { ∅ } )

Proof

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 } ∪ { ∅ } )