Metamath Proof Explorer

Theorem ltslpss

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 ltslpss ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( 𝑋 <s 𝑌 ↔ ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) ) )

Proof

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