Metamath Proof Explorer


Theorem slerec

Description: A comparison law for surreals considered as cuts of sets of surreals. Definition from Conway p. 4. Theorem 4 of Alling p. 186. Theorem 2.5 of Gonshor p. 9. (Contributed by Scott Fenton, 11-Dec-2021)

Ref Expression
Assertion slerec A s B C s D X = A | s B Y = C | s D X s Y d D X < s d a A a < s Y

Proof

Step Hyp Ref Expression
1 scutcl A s B A | s B No
2 1 ad3antrrr A s B C s D A | s B s C | s D d D A | s B No
3 scutcl C s D C | s D No
4 3 ad3antlr A s B C s D A | s B s C | s D d D C | s D No
5 ssltss2 C s D D No
6 5 ad2antlr A s B C s D A | s B s C | s D D No
7 6 sselda A s B C s D A | s B s C | s D d D d No
8 simplr A s B C s D A | s B s C | s D d D A | s B s C | s D
9 scutcut C s D C | s D No C s C | s D C | s D s D
10 9 simp3d C s D C | s D s D
11 10 ad2antlr A s B C s D A | s B s C | s D C | s D s D
12 ssltsep C | s D s D a C | s D d D a < s d
13 11 12 syl A s B C s D A | s B s C | s D a C | s D d D a < s d
14 ovex C | s D V
15 breq1 a = C | s D a < s d C | s D < s d
16 15 ralbidv a = C | s D d D a < s d d D C | s D < s d
17 14 16 ralsn a C | s D d D a < s d d D C | s D < s d
18 13 17 sylib A s B C s D A | s B s C | s D d D C | s D < s d
19 18 r19.21bi A s B C s D A | s B s C | s D d D C | s D < s d
20 2 4 7 8 19 slelttrd A s B C s D A | s B s C | s D d D A | s B < s d
21 20 ralrimiva A s B C s D A | s B s C | s D d D A | s B < s d
22 ssltss1 A s B A No
23 22 adantr A s B C s D A No
24 23 adantr A s B C s D A | s B s C | s D A No
25 24 sselda A s B C s D A | s B s C | s D a A a No
26 1 ad3antrrr A s B C s D A | s B s C | s D a A A | s B No
27 3 ad3antlr A s B C s D A | s B s C | s D a A C | s D No
28 scutcut A s B A | s B No A s A | s B A | s B s B
29 28 simp2d A s B A s A | s B
30 29 adantr A s B C s D A s A | s B
31 30 adantr A s B C s D A | s B s C | s D A s A | s B
32 ssltsep A s A | s B a A d A | s B a < s d
33 31 32 syl A s B C s D A | s B s C | s D a A d A | s B a < s d
34 33 r19.21bi A s B C s D A | s B s C | s D a A d A | s B a < s d
35 ovex A | s B V
36 breq2 d = A | s B a < s d a < s A | s B
37 35 36 ralsn d A | s B a < s d a < s A | s B
38 34 37 sylib A s B C s D A | s B s C | s D a A a < s A | s B
39 simplr A s B C s D A | s B s C | s D a A A | s B s C | s D
40 25 26 27 38 39 sltletrd A s B C s D A | s B s C | s D a A a < s C | s D
41 40 ralrimiva A s B C s D A | s B s C | s D a A a < s C | s D
42 21 41 jca A s B C s D A | s B s C | s D d D A | s B < s d a A a < s C | s D
43 bdayelon bday A | s B On
44 43 onordi Ord bday A | s B
45 ordn2lp Ord bday A | s B ¬ bday A | s B bday C | s D bday C | s D bday A | s B
46 44 45 ax-mp ¬ bday A | s B bday C | s D bday C | s D bday A | s B
47 3 ad2antlr A s B C s D d D A | s B < s d a A a < s C | s D C | s D No
48 1 adantr A s B C s D A | s B No
49 48 adantr A s B C s D d D A | s B < s d a A a < s C | s D A | s B No
50 sltnle C | s D No A | s B No C | s D < s A | s B ¬ A | s B s C | s D
51 47 49 50 syl2anc A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B ¬ A | s B s C | s D
52 3 ad3antlr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C | s D No
53 ssltex1 A s B A V
54 53 ad3antrrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A V
55 snex C | s D V
56 54 55 jctir A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A V C | s D V
57 22 ad3antrrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A No
58 52 snssd A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C | s D No
59 simplrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B a A a < s C | s D
60 breq2 d = C | s D a < s d a < s C | s D
61 14 60 ralsn d C | s D a < s d a < s C | s D
62 61 ralbii a A d C | s D a < s d a A a < s C | s D
63 59 62 sylibr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B a A d C | s D a < s d
64 57 58 63 3jca A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A No C | s D No a A d C | s D a < s d
65 brsslt A s C | s D A V C | s D V A No C | s D No a A d C | s D a < s d
66 56 64 65 sylanbrc A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A s C | s D
67 ssltex2 A s B B V
68 67 ad3antrrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B B V
69 68 55 jctil A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C | s D V B V
70 ssltss2 A s B B No
71 70 ad3antrrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B B No
72 52 adantr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B b B C | s D No
73 48 ad3antrrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B b B A | s B No
74 71 sselda A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B b B b No
75 simplr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B b B C | s D < s A | s B
76 28 simp3d A s B A | s B s B
77 76 ad3antrrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A | s B s B
78 ssltsep A | s B s B a A | s B b B a < s b
79 77 78 syl A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B a A | s B b B a < s b
80 breq1 a = A | s B a < s b A | s B < s b
81 80 ralbidv a = A | s B b B a < s b b B A | s B < s b
82 35 81 ralsn a A | s B b B a < s b b B A | s B < s b
83 79 82 sylib A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B b B A | s B < s b
84 83 r19.21bi A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B b B A | s B < s b
85 72 73 74 75 84 slttrd A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B b B C | s D < s b
86 85 ralrimiva A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B b B C | s D < s b
87 breq1 a = C | s D a < s b C | s D < s b
88 87 ralbidv a = C | s D b B a < s b b B C | s D < s b
89 14 88 ralsn a C | s D b B a < s b b B C | s D < s b
90 86 89 sylibr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B a C | s D b B a < s b
91 58 71 90 3jca A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C | s D No B No a C | s D b B a < s b
92 brsslt C | s D s B C | s D V B V C | s D No B No a C | s D b B a < s b
93 69 91 92 sylanbrc A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C | s D s B
94 sltirr A | s B No ¬ A | s B < s A | s B
95 49 94 syl A s B C s D d D A | s B < s d a A a < s C | s D ¬ A | s B < s A | s B
96 breq1 A | s B = C | s D A | s B < s A | s B C | s D < s A | s B
97 96 notbid A | s B = C | s D ¬ A | s B < s A | s B ¬ C | s D < s A | s B
98 95 97 syl5ibcom A s B C s D d D A | s B < s d a A a < s C | s D A | s B = C | s D ¬ C | s D < s A | s B
99 98 necon2ad A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A | s B C | s D
100 99 imp A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A | s B C | s D
101 100 necomd A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C | s D A | s B
102 scutbdaylt C | s D No A s C | s D C | s D s B C | s D A | s B bday A | s B bday C | s D
103 52 66 93 101 102 syl121anc A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B bday A | s B bday C | s D
104 1 ad3antrrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A | s B No
105 ssltex1 C s D C V
106 105 ad3antlr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C V
107 snex A | s B V
108 106 107 jctir A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C V A | s B V
109 ssltss1 C s D C No
110 109 ad3antlr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C No
111 104 snssd A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A | s B No
112 110 sselda A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C c No
113 52 adantr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C C | s D No
114 48 ad3antrrr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C A | s B No
115 9 simp2d C s D C s C | s D
116 115 ad3antlr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C s C | s D
117 ssltsep C s C | s D c C d C | s D c < s d
118 116 117 syl A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C d C | s D c < s d
119 118 r19.21bi A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C d C | s D c < s d
120 breq2 d = C | s D c < s d c < s C | s D
121 14 120 ralsn d C | s D c < s d c < s C | s D
122 119 121 sylib A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C c < s C | s D
123 simplr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C C | s D < s A | s B
124 112 113 114 122 123 slttrd A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C c < s A | s B
125 breq2 a = A | s B c < s a c < s A | s B
126 35 125 ralsn a A | s B c < s a c < s A | s B
127 124 126 sylibr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C a A | s B c < s a
128 127 ralrimiva A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B c C a A | s B c < s a
129 110 111 128 3jca A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C No A | s B No c C a A | s B c < s a
130 brsslt C s A | s B C V A | s B V C No A | s B No c C a A | s B c < s a
131 108 129 130 sylanbrc A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B C s A | s B
132 ssltex2 C s D D V
133 132 ad3antlr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B D V
134 133 107 jctil A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A | s B V D V
135 5 ad3antlr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B D No
136 simplrl A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B d D A | s B < s d
137 breq1 a = A | s B a < s d A | s B < s d
138 137 ralbidv a = A | s B d D a < s d d D A | s B < s d
139 35 138 ralsn a A | s B d D a < s d d D A | s B < s d
140 136 139 sylibr A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B a A | s B d D a < s d
141 111 135 140 3jca A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A | s B No D No a A | s B d D a < s d
142 brsslt A | s B s D A | s B V D V A | s B No D No a A | s B d D a < s d
143 134 141 142 sylanbrc A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B A | s B s D
144 scutbdaylt A | s B No C s A | s B A | s B s D A | s B C | s D bday C | s D bday A | s B
145 104 131 143 100 144 syl121anc A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B bday C | s D bday A | s B
146 103 145 jca A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B bday A | s B bday C | s D bday C | s D bday A | s B
147 146 ex A s B C s D d D A | s B < s d a A a < s C | s D C | s D < s A | s B bday A | s B bday C | s D bday C | s D bday A | s B
148 51 147 sylbird A s B C s D d D A | s B < s d a A a < s C | s D ¬ A | s B s C | s D bday A | s B bday C | s D bday C | s D bday A | s B
149 46 148 mt3i A s B C s D d D A | s B < s d a A a < s C | s D A | s B s C | s D
150 42 149 impbida A s B C s D A | s B s C | s D d D A | s B < s d a A a < s C | s D
151 breq12 X = A | s B Y = C | s D X s Y A | s B s C | s D
152 breq1 X = A | s B X < s d A | s B < s d
153 152 ralbidv X = A | s B d D X < s d d D A | s B < s d
154 breq2 Y = C | s D a < s Y a < s C | s D
155 154 ralbidv Y = C | s D a A a < s Y a A a < s C | s D
156 153 155 bi2anan9 X = A | s B Y = C | s D d D X < s d a A a < s Y d D A | s B < s d a A a < s C | s D
157 151 156 bibi12d X = A | s B Y = C | s D X s Y d D X < s d a A a < s Y A | s B s C | s D d D A | s B < s d a A a < s C | s D
158 150 157 syl5ibr X = A | s B Y = C | s D A s B C s D X s Y d D X < s d a A a < s Y
159 158 impcom A s B C s D X = A | s B Y = C | s D X s Y d D X < s d a A a < s Y