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 1 𝑜 1 𝑜 2 𝑜 2 𝑜 Or 1 𝑜 2 𝑜

Proof

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