Metamath Proof Explorer

Theorem sltlpss

Description: If two surreals share a birthday, then X iff the left set of X is a proper subset of the left set of Y . (Contributed by Scott Fenton, 17-Sep-2024)

Ref Expression
Assertion sltlpss ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( 𝑋 <s 𝑌 ↔ ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 oldssno ⊢ ( O ‘ ( bday ‘ 𝑋 ) ) ⊆ No
2 1 sseli ⊢ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝑥 ∈ No )
3 2 3ad2ant2 ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) → 𝑥 ∈ No )
4 simp1l1 ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) → 𝑋 ∈ No )
5 simp1l2 ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) → 𝑌 ∈ No )
6 simp3 ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) → 𝑥 <s 𝑋 )
7 simp1r ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) → 𝑋 <s 𝑌 )
8 3 4 5 6 7 slttrd ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) → 𝑥 <s 𝑌 )
9 8 3exp ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → ( 𝑥 <s 𝑋 → 𝑥 <s 𝑌 ) ) )
10 9 imdistand ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑌 ) ) )
11 fveq2 ⊢ ( ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) → ( O ‘ ( bday ‘ 𝑋 ) ) = ( O ‘ ( bday ‘ 𝑌 ) ) )
12 11 3ad2ant3 ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( O ‘ ( bday ‘ 𝑋 ) ) = ( O ‘ ( bday ‘ 𝑌 ) ) )
13 12 adantr ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( O ‘ ( bday ‘ 𝑋 ) ) = ( O ‘ ( bday ‘ 𝑌 ) ) )
14 13 eleq2d ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ) )
15 14 anbi1d ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑌 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) )
16 10 15 sylibd ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) )
17 leftval ⊢ ( L ‘ 𝑋 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 }
18 17 a1i ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( L ‘ 𝑋 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } )
19 18 eleq2d ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( 𝑥 ∈ ( L ‘ 𝑋 ) ↔ 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } ) )
20 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) )
21 19 20 bitrdi ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( 𝑥 ∈ ( L ‘ 𝑋 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) ) )
22 leftval ⊢ ( L ‘ 𝑌 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑥 <s 𝑌 }
23 22 a1i ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( L ‘ 𝑌 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑥 <s 𝑌 } )
24 23 eleq2d ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( 𝑥 ∈ ( L ‘ 𝑌 ) ↔ 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑥 <s 𝑌 } ) )
25 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑥 <s 𝑌 } ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) )
26 24 25 bitrdi ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( 𝑥 ∈ ( L ‘ 𝑌 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) )
27 16 21 26 3imtr4d ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( 𝑥 ∈ ( L ‘ 𝑋 ) → 𝑥 ∈ ( L ‘ 𝑌 ) ) )
28 27 ssrdv ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( L ‘ 𝑋 ) ⊆ ( L ‘ 𝑌 ) )
29 sltirr ⊢ ( 𝑌 ∈ No → ¬ 𝑌 <s 𝑌 )
30 29 3ad2ant2 ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ¬ 𝑌 <s 𝑌 )
31 breq1 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 <s 𝑌 ↔ 𝑌 <s 𝑌 ) )
32 31 notbid ⊢ ( 𝑋 = 𝑌 → ( ¬ 𝑋 <s 𝑌 ↔ ¬ 𝑌 <s 𝑌 ) )
33 30 32 syl5ibrcom ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( 𝑋 = 𝑌 → ¬ 𝑋 <s 𝑌 ) )
34 33 con2d ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( 𝑋 <s 𝑌 → ¬ 𝑋 = 𝑌 ) )
35 34 imp ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ¬ 𝑋 = 𝑌 )
36 simpr ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) )
37 lruneq ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) ∪ ( R ‘ 𝑋 ) ) = ( ( L ‘ 𝑌 ) ∪ ( R ‘ 𝑌 ) ) )
38 37 adantr ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( ( L ‘ 𝑋 ) ∪ ( R ‘ 𝑋 ) ) = ( ( L ‘ 𝑌 ) ∪ ( R ‘ 𝑌 ) ) )
39 38 adantr ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) ∪ ( R ‘ 𝑋 ) ) = ( ( L ‘ 𝑌 ) ∪ ( R ‘ 𝑌 ) ) )
40 39 36 difeq12d ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( ( L ‘ 𝑋 ) ∪ ( R ‘ 𝑋 ) ) ∖ ( L ‘ 𝑋 ) ) = ( ( ( L ‘ 𝑌 ) ∪ ( R ‘ 𝑌 ) ) ∖ ( L ‘ 𝑌 ) ) )
41 difundir ⊢ ( ( ( L ‘ 𝑋 ) ∪ ( R ‘ 𝑋 ) ) ∖ ( L ‘ 𝑋 ) ) = ( ( ( L ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) ∪ ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) )
42 difid ⊢ ( ( L ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) = ∅
43 42 uneq1i ⊢ ( ( ( L ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) ∪ ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) ) = ( ∅ ∪ ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) )
44 0un ⊢ ( ∅ ∪ ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) ) = ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) )
45 41 43 44 3eqtri ⊢ ( ( ( L ‘ 𝑋 ) ∪ ( R ‘ 𝑋 ) ) ∖ ( L ‘ 𝑋 ) ) = ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) )
46 incom ⊢ ( ( L ‘ 𝑋 ) ∩ ( R ‘ 𝑋 ) ) = ( ( R ‘ 𝑋 ) ∩ ( L ‘ 𝑋 ) )
47 simpll1 ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → 𝑋 ∈ No )
48 lltropt ⊢ ( 𝑋 ∈ No → ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) )
49 ssltdisj ⊢ ( ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) → ( ( L ‘ 𝑋 ) ∩ ( R ‘ 𝑋 ) ) = ∅ )
50 47 48 49 3syl ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) ∩ ( R ‘ 𝑋 ) ) = ∅ )
51 46 50 eqtr3id ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( R ‘ 𝑋 ) ∩ ( L ‘ 𝑋 ) ) = ∅ )
52 disjdif2 ⊢ ( ( ( R ‘ 𝑋 ) ∩ ( L ‘ 𝑋 ) ) = ∅ → ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) = ( R ‘ 𝑋 ) )
53 51 52 syl ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) = ( R ‘ 𝑋 ) )
54 45 53 syl5eq ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( ( L ‘ 𝑋 ) ∪ ( R ‘ 𝑋 ) ) ∖ ( L ‘ 𝑋 ) ) = ( R ‘ 𝑋 ) )
55 difundir ⊢ ( ( ( L ‘ 𝑌 ) ∪ ( R ‘ 𝑌 ) ) ∖ ( L ‘ 𝑌 ) ) = ( ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) ∪ ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) )
56 difid ⊢ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) = ∅
57 56 uneq1i ⊢ ( ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) ∪ ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) ) = ( ∅ ∪ ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) )
58 0un ⊢ ( ∅ ∪ ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) ) = ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) )
59 55 57 58 3eqtri ⊢ ( ( ( L ‘ 𝑌 ) ∪ ( R ‘ 𝑌 ) ) ∖ ( L ‘ 𝑌 ) ) = ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) )
60 incom ⊢ ( ( L ‘ 𝑌 ) ∩ ( R ‘ 𝑌 ) ) = ( ( R ‘ 𝑌 ) ∩ ( L ‘ 𝑌 ) )
61 simpll2 ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → 𝑌 ∈ No )
62 lltropt ⊢ ( 𝑌 ∈ No → ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) )
63 ssltdisj ⊢ ( ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) → ( ( L ‘ 𝑌 ) ∩ ( R ‘ 𝑌 ) ) = ∅ )
64 61 62 63 3syl ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑌 ) ∩ ( R ‘ 𝑌 ) ) = ∅ )
65 60 64 eqtr3id ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( R ‘ 𝑌 ) ∩ ( L ‘ 𝑌 ) ) = ∅ )
66 disjdif2 ⊢ ( ( ( R ‘ 𝑌 ) ∩ ( L ‘ 𝑌 ) ) = ∅ → ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) = ( R ‘ 𝑌 ) )
67 65 66 syl ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) = ( R ‘ 𝑌 ) )
68 59 67 syl5eq ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( ( L ‘ 𝑌 ) ∪ ( R ‘ 𝑌 ) ) ∖ ( L ‘ 𝑌 ) ) = ( R ‘ 𝑌 ) )
69 40 54 68 3eqtr3d ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( R ‘ 𝑋 ) = ( R ‘ 𝑌 ) )
70 36 69 oveq12d ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) )
71 lrcut ⊢ ( 𝑋 ∈ No → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )
72 47 71 syl ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )
73 lrcut ⊢ ( 𝑌 ∈ No → ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) = 𝑌 )
74 61 73 syl ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) = 𝑌 )
75 70 72 74 3eqtr3d ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → 𝑋 = 𝑌 )
76 35 75 mtand ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ¬ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) )
77 dfpss2 ⊢ ( ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) ↔ ( ( L ‘ 𝑋 ) ⊆ ( L ‘ 𝑌 ) ∧ ¬ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) )
78 28 76 77 sylanbrc ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) → ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) )
79 78 ex ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( 𝑋 <s 𝑌 → ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) ) )
80 dfpss3 ⊢ ( ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) ↔ ( ( L ‘ 𝑋 ) ⊆ ( L ‘ 𝑌 ) ∧ ¬ ( L ‘ 𝑌 ) ⊆ ( L ‘ 𝑋 ) ) )
81 ssdif0 ⊢ ( ( L ‘ 𝑌 ) ⊆ ( L ‘ 𝑋 ) ↔ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) = ∅ )
82 81 necon3bbii ⊢ ( ¬ ( L ‘ 𝑌 ) ⊆ ( L ‘ 𝑋 ) ↔ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) ≠ ∅ )
83 n0 ⊢ ( ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) )
84 82 83 bitri ⊢ ( ¬ ( L ‘ 𝑌 ) ⊆ ( L ‘ 𝑋 ) ↔ ∃ 𝑥 𝑥 ∈ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) )
85 eldif ⊢ ( 𝑥 ∈ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) ↔ ( 𝑥 ∈ ( L ‘ 𝑌 ) ∧ ¬ 𝑥 ∈ ( L ‘ 𝑋 ) ) )
86 22 a1i ⊢ ( 𝑌 ∈ No → ( L ‘ 𝑌 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑥 <s 𝑌 } )
87 86 eleq2d ⊢ ( 𝑌 ∈ No → ( 𝑥 ∈ ( L ‘ 𝑌 ) ↔ 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑥 <s 𝑌 } ) )
88 87 25 bitrdi ⊢ ( 𝑌 ∈ No → ( 𝑥 ∈ ( L ‘ 𝑌 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) )
89 17 a1i ⊢ ( 𝑋 ∈ No → ( L ‘ 𝑋 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } )
90 89 eleq2d ⊢ ( 𝑋 ∈ No → ( 𝑥 ∈ ( L ‘ 𝑋 ) ↔ 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } ) )
91 90 20 bitrdi ⊢ ( 𝑋 ∈ No → ( 𝑥 ∈ ( L ‘ 𝑋 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) ) )
92 91 notbid ⊢ ( 𝑋 ∈ No → ( ¬ 𝑥 ∈ ( L ‘ 𝑋 ) ↔ ¬ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) ) )
93 ianor ⊢ ( ¬ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) ↔ ( ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∨ ¬ 𝑥 <s 𝑋 ) )
94 92 93 bitrdi ⊢ ( 𝑋 ∈ No → ( ¬ 𝑥 ∈ ( L ‘ 𝑋 ) ↔ ( ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∨ ¬ 𝑥 <s 𝑋 ) ) )
95 88 94 bi2anan9r ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → ( ( 𝑥 ∈ ( L ‘ 𝑌 ) ∧ ¬ 𝑥 ∈ ( L ‘ 𝑋 ) ) ↔ ( ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ∧ ( ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∨ ¬ 𝑥 <s 𝑋 ) ) ) )
96 95 3adant3 ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ( 𝑥 ∈ ( L ‘ 𝑌 ) ∧ ¬ 𝑥 ∈ ( L ‘ 𝑋 ) ) ↔ ( ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ∧ ( ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∨ ¬ 𝑥 <s 𝑋 ) ) ) )
97 simprl ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) )
98 simpl3 ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) )
99 98 fveq2d ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → ( O ‘ ( bday ‘ 𝑋 ) ) = ( O ‘ ( bday ‘ 𝑌 ) ) )
100 97 99 eleqtrrd ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
101 100 pm2.24d ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → ( ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝑋 <s 𝑌 ) )
102 simpll1 ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) ∧ ¬ 𝑥 <s 𝑋 ) → 𝑋 ∈ No )
103 oldssno ⊢ ( O ‘ ( bday ‘ 𝑌 ) ) ⊆ No
104 103 97 sseldi ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → 𝑥 ∈ No )
105 104 adantr ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) ∧ ¬ 𝑥 <s 𝑋 ) → 𝑥 ∈ No )
106 simpll2 ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) ∧ ¬ 𝑥 <s 𝑋 ) → 𝑌 ∈ No )
107 simpl1 ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → 𝑋 ∈ No )
108 slenlt ⊢ ( ( 𝑋 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑋 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝑋 ) )
109 107 104 108 syl2anc ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → ( 𝑋 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝑋 ) )
110 109 biimpar ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) ∧ ¬ 𝑥 <s 𝑋 ) → 𝑋 ≤s 𝑥 )
111 simplrr ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) ∧ ¬ 𝑥 <s 𝑋 ) → 𝑥 <s 𝑌 )
112 102 105 106 110 111 slelttrd ⊢ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) ∧ ¬ 𝑥 <s 𝑋 ) → 𝑋 <s 𝑌 )
113 112 ex ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → ( ¬ 𝑥 <s 𝑋 → 𝑋 <s 𝑌 ) )
114 101 113 jaod ⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ) → ( ( ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∨ ¬ 𝑥 <s 𝑋 ) → 𝑋 <s 𝑌 ) )
115 114 expimpd ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ( ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑥 <s 𝑌 ) ∧ ( ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∨ ¬ 𝑥 <s 𝑋 ) ) → 𝑋 <s 𝑌 ) )
116 96 115 sylbid ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ( 𝑥 ∈ ( L ‘ 𝑌 ) ∧ ¬ 𝑥 ∈ ( L ‘ 𝑋 ) ) → 𝑋 <s 𝑌 ) )
117 85 116 syl5bi ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( 𝑥 ∈ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) → 𝑋 <s 𝑌 ) )
118 117 exlimdv ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ∃ 𝑥 𝑥 ∈ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) → 𝑋 <s 𝑌 ) )
119 84 118 syl5bi ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ¬ ( L ‘ 𝑌 ) ⊆ ( L ‘ 𝑋 ) → 𝑋 <s 𝑌 ) )
120 119 adantld ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ( ( L ‘ 𝑋 ) ⊆ ( L ‘ 𝑌 ) ∧ ¬ ( L ‘ 𝑌 ) ⊆ ( L ‘ 𝑋 ) ) → 𝑋 <s 𝑌 ) )
121 80 120 syl5bi ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) → 𝑋 <s 𝑌 ) )
122 79 121 impbid ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( 𝑋 <s 𝑌 ↔ ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) ) )