Metamath Proof Explorer


Theorem sltrec

Description: A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021)

Ref Expression
Assertion sltrec A s B C s D X = A | s B Y = C | s D X < s Y c C X s c b B b s Y

Proof

Step Hyp Ref Expression
1 simplr A s B C s D X = A | s B Y = C | s D C s D
2 simpll A s B C s D X = A | s B Y = C | s D A s B
3 simprr A s B C s D X = A | s B Y = C | s D Y = C | s D
4 simprl A s B C s D X = A | s B Y = C | s D X = A | s B
5 slerec C s D A s B Y = C | s D X = A | s B Y s X b B Y < s b c C c < s X
6 1 2 3 4 5 syl22anc A s B C s D X = A | s B Y = C | s D Y s X b B Y < s b c C c < s X
7 ancom b B Y < s b c C c < s X c C c < s X b B Y < s b
8 6 7 bitrdi A s B C s D X = A | s B Y = C | s D Y s X c C c < s X b B Y < s b
9 scutcut C s D C | s D No C s C | s D C | s D s D
10 9 simp1d C s D C | s D No
11 10 ad2antlr A s B C s D X = A | s B Y = C | s D C | s D No
12 3 11 eqeltrd A s B C s D X = A | s B Y = C | s D Y No
13 scutcut A s B A | s B No A s A | s B A | s B s B
14 13 simp1d A s B A | s B No
15 14 ad2antrr A s B C s D X = A | s B Y = C | s D A | s B No
16 4 15 eqeltrd A s B C s D X = A | s B Y = C | s D X No
17 slenlt Y No X No Y s X ¬ X < s Y
18 12 16 17 syl2anc A s B C s D X = A | s B Y = C | s D Y s X ¬ X < s Y
19 ssltss1 C s D C No
20 19 ad2antlr A s B C s D X = A | s B Y = C | s D C No
21 20 sselda A s B C s D X = A | s B Y = C | s D c C c No
22 16 adantr A s B C s D X = A | s B Y = C | s D c C X No
23 sltnle c No X No c < s X ¬ X s c
24 21 22 23 syl2anc A s B C s D X = A | s B Y = C | s D c C c < s X ¬ X s c
25 24 ralbidva A s B C s D X = A | s B Y = C | s D c C c < s X c C ¬ X s c
26 12 adantr A s B C s D X = A | s B Y = C | s D b B Y No
27 ssltss2 A s B B No
28 27 ad2antrr A s B C s D X = A | s B Y = C | s D B No
29 28 sselda A s B C s D X = A | s B Y = C | s D b B b No
30 sltnle Y No b No Y < s b ¬ b s Y
31 26 29 30 syl2anc A s B C s D X = A | s B Y = C | s D b B Y < s b ¬ b s Y
32 31 ralbidva A s B C s D X = A | s B Y = C | s D b B Y < s b b B ¬ b s Y
33 25 32 anbi12d A s B C s D X = A | s B Y = C | s D c C c < s X b B Y < s b c C ¬ X s c b B ¬ b s Y
34 ralnex c C ¬ X s c ¬ c C X s c
35 ralnex b B ¬ b s Y ¬ b B b s Y
36 34 35 anbi12i c C ¬ X s c b B ¬ b s Y ¬ c C X s c ¬ b B b s Y
37 ioran ¬ c C X s c b B b s Y ¬ c C X s c ¬ b B b s Y
38 36 37 bitr4i c C ¬ X s c b B ¬ b s Y ¬ c C X s c b B b s Y
39 33 38 bitrdi A s B C s D X = A | s B Y = C | s D c C c < s X b B Y < s b ¬ c C X s c b B b s Y
40 8 18 39 3bitr3d A s B C s D X = A | s B Y = C | s D ¬ X < s Y ¬ c C X s c b B b s Y
41 40 con4bid A s B C s D X = A | s B Y = C | s D X < s Y c C X s c b B b s Y