Metamath Proof Explorer

Theorem slelss

Description: If two surreals A and B share a birthday, then A <_s B if and only if the left set of A is a non-strict subset of the left set of B . (Contributed by Scott Fenton, 21-Mar-2025)

Ref Expression
Assertion slelss 
|- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A <_s B <-> ( _Left ` A ) C_ ( _Left ` B ) ) )

Proof

Step Hyp Ref Expression
1 sltlpss 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A  ( _Left ` A ) C. ( _Left ` B ) ) )
2 fveq2 
 |-  ( A = B -> ( _Left ` A ) = ( _Left ` B ) )
3 simpr 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( _Left ` A ) = ( _Left ` B ) )
4 lruneq 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( ( _Left ` B ) u. ( _Right ` B ) ) )
5 4 adantr 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( ( _Left ` B ) u. ( _Right ` B ) ) )
6 5 3 difeq12d 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) )
7 difundir 
 |-  ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( ( _Left ` A ) \ ( _Left ` A ) ) u. ( ( _Right ` A ) \ ( _Left ` A ) ) )
8 difid 
 |-  ( ( _Left ` A ) \ ( _Left ` A ) ) = (/)
9 8 uneq1i 
 |-  ( ( ( _Left ` A ) \ ( _Left ` A ) ) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) = ( (/) u. ( ( _Right ` A ) \ ( _Left ` A ) ) )
10 0un 
 |-  ( (/) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) = ( ( _Right ` A ) \ ( _Left ` A ) )
11 7 9 10 3eqtri 
 |-  ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( _Right ` A ) \ ( _Left ` A ) )
12 incom 
 |-  ( ( _Left ` A ) i^i ( _Right ` A ) ) = ( ( _Right ` A ) i^i ( _Left ` A ) )
13 lltropt 
 |-  ( _Left ` A ) <
14 ssltdisj 
 |-  ( ( _Left ` A ) < ( ( _Left ` A ) i^i ( _Right ` A ) ) = (/) )
15 13 14 mp1i 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) i^i ( _Right ` A ) ) = (/) )
16 12 15 eqtr3id 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` A ) i^i ( _Left ` A ) ) = (/) )
17 disjdif2 
 |-  ( ( ( _Right ` A ) i^i ( _Left ` A ) ) = (/) -> ( ( _Right ` A ) \ ( _Left ` A ) ) = ( _Right ` A ) )
18 16 17 syl 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` A ) \ ( _Left ` A ) ) = ( _Right ` A ) )
19 11 18 eqtrid 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( _Right ` A ) )
20 difundir 
 |-  ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( ( ( _Left ` B ) \ ( _Left ` B ) ) u. ( ( _Right ` B ) \ ( _Left ` B ) ) )
21 difid 
 |-  ( ( _Left ` B ) \ ( _Left ` B ) ) = (/)
22 21 uneq1i 
 |-  ( ( ( _Left ` B ) \ ( _Left ` B ) ) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) = ( (/) u. ( ( _Right ` B ) \ ( _Left ` B ) ) )
23 0un 
 |-  ( (/) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) = ( ( _Right ` B ) \ ( _Left ` B ) )
24 20 22 23 3eqtri 
 |-  ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( ( _Right ` B ) \ ( _Left ` B ) )
25 incom 
 |-  ( ( _Left ` B ) i^i ( _Right ` B ) ) = ( ( _Right ` B ) i^i ( _Left ` B ) )
26 lltropt 
 |-  ( _Left ` B ) <
27 ssltdisj 
 |-  ( ( _Left ` B ) < ( ( _Left ` B ) i^i ( _Right ` B ) ) = (/) )
28 26 27 mp1i 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` B ) i^i ( _Right ` B ) ) = (/) )
29 25 28 eqtr3id 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` B ) i^i ( _Left ` B ) ) = (/) )
30 disjdif2 
 |-  ( ( ( _Right ` B ) i^i ( _Left ` B ) ) = (/) -> ( ( _Right ` B ) \ ( _Left ` B ) ) = ( _Right ` B ) )
31 29 30 syl 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` B ) \ ( _Left ` B ) ) = ( _Right ` B ) )
32 24 31 eqtrid 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( _Right ` B ) )
33 6 19 32 3eqtr3d 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( _Right ` A ) = ( _Right ` B ) )
34 3 33 oveq12d 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( ( _Left ` B ) |s ( _Right ` B ) ) )
35 simpl1 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> A e. No )
36 lrcut 
 |-  ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
37 35 36 syl 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
38 simpl2 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> B e. No )
39 lrcut 
 |-  ( B e. No -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B )
40 38 39 syl 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B )
41 34 37 40 3eqtr3d 
 |-  ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> A = B )
42 41 ex 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) = ( _Left ` B ) -> A = B ) )
43 2 42 impbid2 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A = B <-> ( _Left ` A ) = ( _Left ` B ) ) )
44 1 43 orbi12d 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( A  ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) ) )
45 sleloe 
 |-  ( ( A e. No /\ B e. No ) -> ( A <_s B <-> ( A
46 45 3adant3 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A <_s B <-> ( A
47 sspss 
 |-  ( ( _Left ` A ) C_ ( _Left ` B ) <-> ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) )
48 47 a1i 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) C_ ( _Left ` B ) <-> ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) ) )
49 44 46 48 3bitr4d 
 |-  ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A <_s B <-> ( _Left ` A ) C_ ( _Left ` B ) ) )