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 ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( 𝐴 ≤s 𝐵 ↔ ( L ‘ 𝐴 ) ⊆ ( L ‘ 𝐵 ) ) )

Proof

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