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