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 < ( X <_s Y <-> ( A. d e. D X

Proof

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