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 No B No bday A = bday B A s B L A L B

Proof

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