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 } u. { (/) } )

Proof

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