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 lltropt âŠĒ ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 )
48 ssltdisj âŠĒ ( ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) → ( ( L ‘ 𝑋 ) âˆĐ ( R ‘ 𝑋 ) ) = ∅ )
49 47 48 mp1i âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) âˆĐ ( R ‘ 𝑋 ) ) = ∅ )
50 46 49 eqtr3id âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( R ‘ 𝑋 ) âˆĐ ( L ‘ 𝑋 ) ) = ∅ )
51 disjdif2 âŠĒ ( ( ( R ‘ 𝑋 ) âˆĐ ( L ‘ 𝑋 ) ) = ∅ → ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) = ( R ‘ 𝑋 ) )
52 50 51 syl âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( R ‘ 𝑋 ) ∖ ( L ‘ 𝑋 ) ) = ( R ‘ 𝑋 ) )
53 45 52 eqtrid âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( ( L ‘ 𝑋 ) ∊ ( R ‘ 𝑋 ) ) ∖ ( L ‘ 𝑋 ) ) = ( R ‘ 𝑋 ) )
54 difundir âŠĒ ( ( ( L ‘ 𝑌 ) ∊ ( R ‘ 𝑌 ) ) ∖ ( L ‘ 𝑌 ) ) = ( ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) ∊ ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) )
55 difid âŠĒ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) = ∅
56 55 uneq1i âŠĒ ( ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) ∊ ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) ) = ( ∅ ∊ ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) )
57 0un âŠĒ ( ∅ ∊ ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) ) = ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) )
58 54 56 57 3eqtri âŠĒ ( ( ( L ‘ 𝑌 ) ∊ ( R ‘ 𝑌 ) ) ∖ ( L ‘ 𝑌 ) ) = ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) )
59 incom âŠĒ ( ( L ‘ 𝑌 ) âˆĐ ( R ‘ 𝑌 ) ) = ( ( R ‘ 𝑌 ) âˆĐ ( L ‘ 𝑌 ) )
60 lltropt âŠĒ ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 )
61 ssltdisj âŠĒ ( ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) → ( ( L ‘ 𝑌 ) âˆĐ ( R ‘ 𝑌 ) ) = ∅ )
62 60 61 mp1i âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑌 ) âˆĐ ( R ‘ 𝑌 ) ) = ∅ )
63 59 62 eqtr3id âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( R ‘ 𝑌 ) âˆĐ ( L ‘ 𝑌 ) ) = ∅ )
64 disjdif2 âŠĒ ( ( ( R ‘ 𝑌 ) âˆĐ ( L ‘ 𝑌 ) ) = ∅ → ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) = ( R ‘ 𝑌 ) )
65 63 64 syl âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( R ‘ 𝑌 ) ∖ ( L ‘ 𝑌 ) ) = ( R ‘ 𝑌 ) )
66 58 65 eqtrid âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( ( L ‘ 𝑌 ) ∊ ( R ‘ 𝑌 ) ) ∖ ( L ‘ 𝑌 ) ) = ( R ‘ 𝑌 ) )
67 40 53 66 3eqtr3d âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( R ‘ 𝑋 ) = ( R ‘ 𝑌 ) )
68 36 67 oveq12d âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) )
69 simpll1 âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → 𝑋 ∈ No )
70 lrcut âŠĒ ( 𝑋 ∈ No → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )
71 69 70 syl âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )
72 simpll2 âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → 𝑌 ∈ No )
73 lrcut âŠĒ ( 𝑌 ∈ No → ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) = 𝑌 )
74 72 73 syl âŠĒ ( ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) ∧ 𝑋 <s 𝑌 ) ∧ ( L ‘ 𝑋 ) = ( L ‘ 𝑌 ) ) → ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) = 𝑌 )
75 68 71 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 sselid âŠĒ ( ( ( 𝑋 ∈ 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 biimtrid âŠĒ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ð‘Ĩ ∈ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) → 𝑋 <s 𝑌 ) )
118 117 exlimdv âŠĒ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ∃ ð‘Ĩ ð‘Ĩ ∈ ( ( L ‘ 𝑌 ) ∖ ( L ‘ 𝑋 ) ) → 𝑋 <s 𝑌 ) )
119 84 118 biimtrid âŠĒ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ÂŽ ( L ‘ 𝑌 ) ⊆ ( L ‘ 𝑋 ) → 𝑋 <s 𝑌 ) )
120 119 adantld âŠĒ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ( ( L ‘ 𝑋 ) ⊆ ( L ‘ 𝑌 ) ∧ ÂŽ ( L ‘ 𝑌 ) ⊆ ( L ‘ 𝑋 ) ) → 𝑋 <s 𝑌 ) )
121 80 120 biimtrid âŠĒ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) → 𝑋 <s 𝑌 ) )
122 79 121 impbid âŠĒ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘ 𝑋 ) = ( bday ‘ 𝑌 ) ) → ( 𝑋 <s 𝑌 ↔ ( L ‘ 𝑋 ) ⊊ ( L ‘ 𝑌 ) ) )