MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sltlpss Structured version   Visualization version   GIF version

Theorem sltlpss 27638
Description: If two surreals share a birthday, then 𝑋 <s 𝑌 iff the left set of 𝑋 is a proper subset of the left set of 𝑌. (Contributed by Scott Fenton, 17-Sep-2024.)
Assertion
Ref Expression
sltlpss ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 ↔ ( L ‘𝑋) ⊊ ( L ‘𝑌)))

Proof of Theorem sltlpss
Dummy variable ð‘Ĩ is distinct from all other variables.
StepHypRef Expression
1 oldssno 27593 . . . . . . . . . . . 12 ( O ‘( bday ‘𝑋)) ⊆ No
21sseli 3977 . . . . . . . . . . 11 (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) → ð‘Ĩ ∈ No )
323ad2ant2 1132 . . . . . . . . . 10 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) → ð‘Ĩ ∈ No )
4 simp1l1 1264 . . . . . . . . . 10 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) → 𝑋 ∈ No )
5 simp1l2 1265 . . . . . . . . . 10 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) → 𝑌 ∈ No )
6 simp3 1136 . . . . . . . . . 10 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) → ð‘Ĩ <s 𝑋)
7 simp1r 1196 . . . . . . . . . 10 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) → 𝑋 <s 𝑌)
83, 4, 5, 6, 7slttrd 27498 . . . . . . . . 9 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) → ð‘Ĩ <s 𝑌)
983exp 1117 . . . . . . . 8 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) → (ð‘Ĩ <s 𝑋 → ð‘Ĩ <s 𝑌)))
109imdistand 569 . . . . . . 7 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) → (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑌)))
11 fveq2 6890 . . . . . . . . . . 11 (( bday ‘𝑋) = ( bday ‘𝑌) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
12113ad2ant3 1133 . . . . . . . . . 10 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
1312adantr 479 . . . . . . . . 9 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
1413eleq2d 2817 . . . . . . . 8 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ↔ ð‘Ĩ ∈ ( O ‘( bday ‘𝑌))))
1514anbi1d 628 . . . . . . 7 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑌) ↔ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)))
1610, 15sylibd 238 . . . . . 6 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) → (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)))
17 leftval 27595 . . . . . . . . 9 ( L ‘𝑋) = {ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĢ ð‘Ĩ <s 𝑋}
1817a1i 11 . . . . . . . 8 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) = {ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĢ ð‘Ĩ <s 𝑋})
1918eleq2d 2817 . . . . . . 7 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (ð‘Ĩ ∈ ( L ‘𝑋) ↔ ð‘Ĩ ∈ {ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĢ ð‘Ĩ <s 𝑋}))
20 rabid 3450 . . . . . . 7 (ð‘Ĩ ∈ {ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĢ ð‘Ĩ <s 𝑋} ↔ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋))
2119, 20bitrdi 286 . . . . . 6 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (ð‘Ĩ ∈ ( L ‘𝑋) ↔ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋)))
22 leftval 27595 . . . . . . . . 9 ( L ‘𝑌) = {ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) âˆĢ ð‘Ĩ <s 𝑌}
2322a1i 11 . . . . . . . 8 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑌) = {ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) âˆĢ ð‘Ĩ <s 𝑌})
2423eleq2d 2817 . . . . . . 7 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (ð‘Ĩ ∈ ( L ‘𝑌) ↔ ð‘Ĩ ∈ {ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) âˆĢ ð‘Ĩ <s 𝑌}))
25 rabid 3450 . . . . . . 7 (ð‘Ĩ ∈ {ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) âˆĢ ð‘Ĩ <s 𝑌} ↔ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌))
2624, 25bitrdi 286 . . . . . 6 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (ð‘Ĩ ∈ ( L ‘𝑌) ↔ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)))
2716, 21, 263imtr4d 293 . . . . 5 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (ð‘Ĩ ∈ ( L ‘𝑋) → ð‘Ĩ ∈ ( L ‘𝑌)))
2827ssrdv 3987 . . . 4 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) ⊆ ( L ‘𝑌))
29 sltirr 27485 . . . . . . . . 9 (𝑌 ∈ No → ÂŽ 𝑌 <s 𝑌)
30293ad2ant2 1132 . . . . . . . 8 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ÂŽ 𝑌 <s 𝑌)
31 breq1 5150 . . . . . . . . 9 (𝑋 = 𝑌 → (𝑋 <s 𝑌 ↔ 𝑌 <s 𝑌))
3231notbid 317 . . . . . . . 8 (𝑋 = 𝑌 → (ÂŽ 𝑋 <s 𝑌 ↔ ÂŽ 𝑌 <s 𝑌))
3330, 32syl5ibrcom 246 . . . . . . 7 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 = 𝑌 → ÂŽ 𝑋 <s 𝑌))
3433con2d 134 . . . . . 6 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 → ÂŽ 𝑋 = 𝑌))
3534imp 405 . . . . 5 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ÂŽ 𝑋 = 𝑌)
36 simpr 483 . . . . . . 7 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ( L ‘𝑋) = ( L ‘𝑌))
37 lruneq 27637 . . . . . . . . . . 11 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ∊ ( R ‘𝑋)) = (( L ‘𝑌) ∊ ( R ‘𝑌)))
3837adantr 479 . . . . . . . . . 10 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (( L ‘𝑋) ∊ ( R ‘𝑋)) = (( L ‘𝑌) ∊ ( R ‘𝑌)))
3938adantr 479 . . . . . . . . 9 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) ∊ ( R ‘𝑋)) = (( L ‘𝑌) ∊ ( R ‘𝑌)))
4039, 36difeq12d 4122 . . . . . . . 8 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑋) ∊ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ((( L ‘𝑌) ∊ ( R ‘𝑌)) ∖ ( L ‘𝑌)))
41 difundir 4279 . . . . . . . . . 10 ((( L ‘𝑋) ∊ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ((( L ‘𝑋) ∖ ( L ‘𝑋)) ∊ (( R ‘𝑋) ∖ ( L ‘𝑋)))
42 difid 4369 . . . . . . . . . . 11 (( L ‘𝑋) ∖ ( L ‘𝑋)) = ∅
4342uneq1i 4158 . . . . . . . . . 10 ((( L ‘𝑋) ∖ ( L ‘𝑋)) ∊ (( R ‘𝑋) ∖ ( L ‘𝑋))) = (∅ ∊ (( R ‘𝑋) ∖ ( L ‘𝑋)))
44 0un 4391 . . . . . . . . . 10 (∅ ∊ (( R ‘𝑋) ∖ ( L ‘𝑋))) = (( R ‘𝑋) ∖ ( L ‘𝑋))
4541, 43, 443eqtri 2762 . . . . . . . . 9 ((( L ‘𝑋) ∊ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = (( R ‘𝑋) ∖ ( L ‘𝑋))
46 incom 4200 . . . . . . . . . . 11 (( L ‘𝑋) âˆĐ ( R ‘𝑋)) = (( R ‘𝑋) âˆĐ ( L ‘𝑋))
47 lltropt 27604 . . . . . . . . . . . 12 ( L ‘𝑋) <<s ( R ‘𝑋)
48 ssltdisj 27559 . . . . . . . . . . . 12 (( L ‘𝑋) <<s ( R ‘𝑋) → (( L ‘𝑋) âˆĐ ( R ‘𝑋)) = ∅)
4947, 48mp1i 13 . . . . . . . . . . 11 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) âˆĐ ( R ‘𝑋)) = ∅)
5046, 49eqtr3id 2784 . . . . . . . . . 10 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑋) âˆĐ ( L ‘𝑋)) = ∅)
51 disjdif2 4478 . . . . . . . . . 10 ((( R ‘𝑋) âˆĐ ( L ‘𝑋)) = ∅ → (( R ‘𝑋) ∖ ( L ‘𝑋)) = ( R ‘𝑋))
5250, 51syl 17 . . . . . . . . 9 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑋) ∖ ( L ‘𝑋)) = ( R ‘𝑋))
5345, 52eqtrid 2782 . . . . . . . 8 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑋) ∊ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ( R ‘𝑋))
54 difundir 4279 . . . . . . . . . 10 ((( L ‘𝑌) ∊ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = ((( L ‘𝑌) ∖ ( L ‘𝑌)) ∊ (( R ‘𝑌) ∖ ( L ‘𝑌)))
55 difid 4369 . . . . . . . . . . 11 (( L ‘𝑌) ∖ ( L ‘𝑌)) = ∅
5655uneq1i 4158 . . . . . . . . . 10 ((( L ‘𝑌) ∖ ( L ‘𝑌)) ∊ (( R ‘𝑌) ∖ ( L ‘𝑌))) = (∅ ∊ (( R ‘𝑌) ∖ ( L ‘𝑌)))
57 0un 4391 . . . . . . . . . 10 (∅ ∊ (( R ‘𝑌) ∖ ( L ‘𝑌))) = (( R ‘𝑌) ∖ ( L ‘𝑌))
5854, 56, 573eqtri 2762 . . . . . . . . 9 ((( L ‘𝑌) ∊ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = (( R ‘𝑌) ∖ ( L ‘𝑌))
59 incom 4200 . . . . . . . . . . 11 (( L ‘𝑌) âˆĐ ( R ‘𝑌)) = (( R ‘𝑌) âˆĐ ( L ‘𝑌))
60 lltropt 27604 . . . . . . . . . . . 12 ( L ‘𝑌) <<s ( R ‘𝑌)
61 ssltdisj 27559 . . . . . . . . . . . 12 (( L ‘𝑌) <<s ( R ‘𝑌) → (( L ‘𝑌) âˆĐ ( R ‘𝑌)) = ∅)
6260, 61mp1i 13 . . . . . . . . . . 11 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑌) âˆĐ ( R ‘𝑌)) = ∅)
6359, 62eqtr3id 2784 . . . . . . . . . 10 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑌) âˆĐ ( L ‘𝑌)) = ∅)
64 disjdif2 4478 . . . . . . . . . 10 ((( R ‘𝑌) âˆĐ ( L ‘𝑌)) = ∅ → (( R ‘𝑌) ∖ ( L ‘𝑌)) = ( R ‘𝑌))
6563, 64syl 17 . . . . . . . . 9 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑌) ∖ ( L ‘𝑌)) = ( R ‘𝑌))
6658, 65eqtrid 2782 . . . . . . . 8 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑌) ∊ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = ( R ‘𝑌))
6740, 53, 663eqtr3d 2778 . . . . . . 7 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ( R ‘𝑋) = ( R ‘𝑌))
6836, 67oveq12d 7429 . . . . . 6 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) |s ( R ‘𝑋)) = (( L ‘𝑌) |s ( R ‘𝑌)))
69 simpll1 1210 . . . . . . 7 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑋 ∈ No )
70 lrcut 27634 . . . . . . 7 (𝑋 ∈ No → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
7169, 70syl 17 . . . . . 6 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋)
72 simpll2 1211 . . . . . . 7 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑌 ∈ No )
73 lrcut 27634 . . . . . . 7 (𝑌 ∈ No → (( L ‘𝑌) |s ( R ‘𝑌)) = 𝑌)
7472, 73syl 17 . . . . . 6 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑌) |s ( R ‘𝑌)) = 𝑌)
7568, 71, 743eqtr3d 2778 . . . . 5 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑋 = 𝑌)
7635, 75mtand 812 . . . 4 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ÂŽ ( L ‘𝑋) = ( L ‘𝑌))
77 dfpss2 4084 . . . 4 (( L ‘𝑋) ⊊ ( L ‘𝑌) ↔ (( L ‘𝑋) ⊆ ( L ‘𝑌) ∧ ÂŽ ( L ‘𝑋) = ( L ‘𝑌)))
7828, 76, 77sylanbrc 581 . . 3 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) ⊊ ( L ‘𝑌))
7978ex 411 . 2 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 → ( L ‘𝑋) ⊊ ( L ‘𝑌)))
80 dfpss3 4085 . . 3 (( L ‘𝑋) ⊊ ( L ‘𝑌) ↔ (( L ‘𝑋) ⊆ ( L ‘𝑌) ∧ ÂŽ ( L ‘𝑌) ⊆ ( L ‘𝑋)))
81 ssdif0 4362 . . . . . . 7 (( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ (( L ‘𝑌) ∖ ( L ‘𝑋)) = ∅)
8281necon3bbii 2986 . . . . . 6 (ÂŽ ( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ (( L ‘𝑌) ∖ ( L ‘𝑋)) ≠ ∅)
83 n0 4345 . . . . . 6 ((( L ‘𝑌) ∖ ( L ‘𝑋)) ≠ ∅ ↔ ∃ð‘Ĩ ð‘Ĩ ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)))
8482, 83bitri 274 . . . . 5 (ÂŽ ( L ‘𝑌) ⊆ ( L ‘𝑋) ↔ ∃ð‘Ĩ ð‘Ĩ ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)))
85 eldif 3957 . . . . . . 7 (ð‘Ĩ ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) ↔ (ð‘Ĩ ∈ ( L ‘𝑌) ∧ ÂŽ ð‘Ĩ ∈ ( L ‘𝑋)))
8622a1i 11 . . . . . . . . . . . 12 (𝑌 ∈ No → ( L ‘𝑌) = {ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) âˆĢ ð‘Ĩ <s 𝑌})
8786eleq2d 2817 . . . . . . . . . . 11 (𝑌 ∈ No → (ð‘Ĩ ∈ ( L ‘𝑌) ↔ ð‘Ĩ ∈ {ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) âˆĢ ð‘Ĩ <s 𝑌}))
8887, 25bitrdi 286 . . . . . . . . . 10 (𝑌 ∈ No → (ð‘Ĩ ∈ ( L ‘𝑌) ↔ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)))
8917a1i 11 . . . . . . . . . . . . . 14 (𝑋 ∈ No → ( L ‘𝑋) = {ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĢ ð‘Ĩ <s 𝑋})
9089eleq2d 2817 . . . . . . . . . . . . 13 (𝑋 ∈ No → (ð‘Ĩ ∈ ( L ‘𝑋) ↔ ð‘Ĩ ∈ {ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĢ ð‘Ĩ <s 𝑋}))
9190, 20bitrdi 286 . . . . . . . . . . . 12 (𝑋 ∈ No → (ð‘Ĩ ∈ ( L ‘𝑋) ↔ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋)))
9291notbid 317 . . . . . . . . . . 11 (𝑋 ∈ No → (ÂŽ ð‘Ĩ ∈ ( L ‘𝑋) ↔ ÂŽ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋)))
93 ianor 978 . . . . . . . . . . 11 (ÂŽ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) ∧ ð‘Ĩ <s 𝑋) ↔ (ÂŽ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĻ ÂŽ ð‘Ĩ <s 𝑋))
9492, 93bitrdi 286 . . . . . . . . . 10 (𝑋 ∈ No → (ÂŽ ð‘Ĩ ∈ ( L ‘𝑋) ↔ (ÂŽ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĻ ÂŽ ð‘Ĩ <s 𝑋)))
9588, 94bi2anan9r 636 . . . . . . . . 9 ((𝑋 ∈ No ∧ 𝑌 ∈ No ) → ((ð‘Ĩ ∈ ( L ‘𝑌) ∧ ÂŽ ð‘Ĩ ∈ ( L ‘𝑋)) ↔ ((ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌) ∧ (ÂŽ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĻ ÂŽ ð‘Ĩ <s 𝑋))))
96953adant3 1130 . . . . . . . 8 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ((ð‘Ĩ ∈ ( L ‘𝑌) ∧ ÂŽ ð‘Ĩ ∈ ( L ‘𝑋)) ↔ ((ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌) ∧ (ÂŽ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĻ ÂŽ ð‘Ĩ <s 𝑋))))
97 simprl 767 . . . . . . . . . . . 12 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)))
98 simpl3 1191 . . . . . . . . . . . . 13 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → ( bday ‘𝑋) = ( bday ‘𝑌))
9998fveq2d 6894 . . . . . . . . . . . 12 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday ‘𝑌)))
10097, 99eleqtrrd 2834 . . . . . . . . . . 11 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)))
101100pm2.24d 151 . . . . . . . . . 10 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → (ÂŽ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) → 𝑋 <s 𝑌))
102 simpll1 1210 . . . . . . . . . . . 12 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) ∧ ÂŽ ð‘Ĩ <s 𝑋) → 𝑋 ∈ No )
103 oldssno 27593 . . . . . . . . . . . . . 14 ( O ‘( bday ‘𝑌)) ⊆ No
104103, 97sselid 3979 . . . . . . . . . . . . 13 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → ð‘Ĩ ∈ No )
105104adantr 479 . . . . . . . . . . . 12 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) ∧ ÂŽ ð‘Ĩ <s 𝑋) → ð‘Ĩ ∈ No )
106 simpll2 1211 . . . . . . . . . . . 12 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) ∧ ÂŽ ð‘Ĩ <s 𝑋) → 𝑌 ∈ No )
107 simpl1 1189 . . . . . . . . . . . . . 14 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → 𝑋 ∈ No )
108 slenlt 27491 . . . . . . . . . . . . . 14 ((𝑋 ∈ No ∧ ð‘Ĩ ∈ No ) → (𝑋 â‰Īs ð‘Ĩ ↔ ÂŽ ð‘Ĩ <s 𝑋))
109107, 104, 108syl2anc 582 . . . . . . . . . . . . 13 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → (𝑋 â‰Īs ð‘Ĩ ↔ ÂŽ ð‘Ĩ <s 𝑋))
110109biimpar 476 . . . . . . . . . . . 12 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) ∧ ÂŽ ð‘Ĩ <s 𝑋) → 𝑋 â‰Īs ð‘Ĩ)
111 simplrr 774 . . . . . . . . . . . 12 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) ∧ ÂŽ ð‘Ĩ <s 𝑋) → ð‘Ĩ <s 𝑌)
112102, 105, 106, 110, 111slelttrd 27500 . . . . . . . . . . 11 ((((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) ∧ ÂŽ ð‘Ĩ <s 𝑋) → 𝑋 <s 𝑌)
113112ex 411 . . . . . . . . . 10 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → (ÂŽ ð‘Ĩ <s 𝑋 → 𝑋 <s 𝑌))
114101, 113jaod 855 . . . . . . . . 9 (((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) ∧ (ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌)) → ((ÂŽ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĻ ÂŽ ð‘Ĩ <s 𝑋) → 𝑋 <s 𝑌))
115114expimpd 452 . . . . . . . 8 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (((ð‘Ĩ ∈ ( O ‘( bday ‘𝑌)) ∧ ð‘Ĩ <s 𝑌) ∧ (ÂŽ ð‘Ĩ ∈ ( O ‘( bday ‘𝑋)) âˆĻ ÂŽ ð‘Ĩ <s 𝑋)) → 𝑋 <s 𝑌))
11696, 115sylbid 239 . . . . . . 7 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ((ð‘Ĩ ∈ ( L ‘𝑌) ∧ ÂŽ ð‘Ĩ ∈ ( L ‘𝑋)) → 𝑋 <s 𝑌))
11785, 116biimtrid 241 . . . . . 6 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (ð‘Ĩ ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) → 𝑋 <s 𝑌))
118117exlimdv 1934 . . . . 5 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (∃ð‘Ĩ ð‘Ĩ ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) → 𝑋 <s 𝑌))
11984, 118biimtrid 241 . . . 4 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (ÂŽ ( L ‘𝑌) ⊆ ( L ‘𝑋) → 𝑋 <s 𝑌))
120119adantld 489 . . 3 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → ((( L ‘𝑋) ⊆ ( L ‘𝑌) ∧ ÂŽ ( L ‘𝑌) ⊆ ( L ‘𝑋)) → 𝑋 <s 𝑌))
12180, 120biimtrid 241 . 2 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ⊊ ( L ‘𝑌) → 𝑋 <s 𝑌))
12279, 121impbid 211 1 ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 ↔ ( L ‘𝑋) ⊊ ( L ‘𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ÂŽ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   âˆĻ wo 843   ∧ w3a 1085   = wceq 1539  âˆƒwex 1779   ∈ wcel 2104   ≠ wne 2938  {crab 3430   ∖ cdif 3944   ∊ cun 3945   âˆĐ cin 3946   ⊆ wss 3947   ⊊ wpss 3948  âˆ…c0 4321   class class class wbr 5147  â€˜cfv 6542  (class class class)co 7411   No csur 27379   <s cslt 27380   bday cbday 27381   â‰Īs csle 27483   <<s csslt 27518   |s cscut 27520   O cold 27575   L cleft 27577   R cright 27578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-1o 8468  df-2o 8469  df-no 27382  df-slt 27383  df-bday 27384  df-sle 27484  df-sslt 27519  df-scut 27521  df-made 27579  df-old 27580  df-left 27582  df-right 27583
This theorem is referenced by:  slelss  27639
  Copyright terms: Public domain W3C validator