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 syl5ibr
 |-  ( ( 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