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 < ( X  ( E. c e. C X <_s c \/ E. b e. B b <_s Y ) ) )

Proof

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