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

Theorem mulsproplem14 27498
Description: Lemma for surreal multiplication. Finally, we remove the restriction on ๐ธ and ๐น from mulsproplem12 27496 and mulsproplem13 27497. This completes the induction on surreal multiplication. mulsprop 27499 brings all this together technically. (Contributed by Scott Fenton, 5-Mar-2025.)
Hypotheses
Ref Expression
mulsproplem.1 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
mulsproplem.2 (๐œ‘ โ†’ ๐ถ โˆˆ No )
mulsproplem.3 (๐œ‘ โ†’ ๐ท โˆˆ No )
mulsproplem.4 (๐œ‘ โ†’ ๐ธ โˆˆ No )
mulsproplem.5 (๐œ‘ โ†’ ๐น โˆˆ No )
mulsproplem.6 (๐œ‘ โ†’ ๐ถ <s ๐ท)
mulsproplem.7 (๐œ‘ โ†’ ๐ธ <s ๐น)
Assertion
Ref Expression
mulsproplem14 (๐œ‘ โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ต,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ถ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ท,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ธ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐น,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“
Allowed substitution hints:   ๐œ‘(๐‘’,๐‘“,๐‘Ž,๐‘,๐‘,๐‘‘)

Proof of Theorem mulsproplem14
Dummy variables ๐‘” โ„Ž ๐‘– ๐‘— ๐‘˜ ๐‘™ ๐‘ฅ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulsproplem.1 . . . 4 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
21adantr 481 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
3 mulsproplem.2 . . . 4 (๐œ‘ โ†’ ๐ถ โˆˆ No )
43adantr 481 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ถ โˆˆ No )
5 mulsproplem.3 . . . 4 (๐œ‘ โ†’ ๐ท โˆˆ No )
65adantr 481 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ท โˆˆ No )
7 mulsproplem.4 . . . 4 (๐œ‘ โ†’ ๐ธ โˆˆ No )
87adantr 481 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ธ โˆˆ No )
9 mulsproplem.5 . . . 4 (๐œ‘ โ†’ ๐น โˆˆ No )
109adantr 481 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐น โˆˆ No )
11 mulsproplem.6 . . . 4 (๐œ‘ โ†’ ๐ถ <s ๐ท)
1211adantr 481 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ถ <s ๐ท)
13 mulsproplem.7 . . . 4 (๐œ‘ โ†’ ๐ธ <s ๐น)
1413adantr 481 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ๐ธ <s ๐น)
15 simpr 485 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
162, 4, 6, 8, 10, 12, 14, 15mulsproplem13 27497 . 2 ((๐œ‘ โˆง (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
177adantr 481 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ๐ธ โˆˆ No )
189adantr 481 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ๐น โˆˆ No )
19 simpr 485 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ( bday โ€˜๐ธ) = ( bday โ€˜๐น))
2013adantr 481 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ๐ธ <s ๐น)
21 nodense 27122 . . . 4 (((๐ธ โˆˆ No โˆง ๐น โˆˆ No ) โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง ๐ธ <s ๐น)) โ†’ โˆƒ๐‘ฅ โˆˆ No (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))
2217, 18, 19, 20, 21syl22anc 837 . . 3 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ โˆƒ๐‘ฅ โˆˆ No (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))
23 unidm 4148 . . . . . . . . . . . . . . . . 17 (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )))) = ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )))
24 unidm 4148 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) = (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))
25 bday0s 27255 . . . . . . . . . . . . . . . . . . 19 ( bday โ€˜ 0s ) = โˆ…
2625, 25oveq12i 7405 . . . . . . . . . . . . . . . . . 18 (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) = (โˆ… +no โˆ…)
27 0elon 6407 . . . . . . . . . . . . . . . . . . 19 โˆ… โˆˆ On
28 naddrid 8665 . . . . . . . . . . . . . . . . . . 19 (โˆ… โˆˆ On โ†’ (โˆ… +no โˆ…) = โˆ…)
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . 18 (โˆ… +no โˆ…) = โˆ…
3026, 29eqtri 2759 . . . . . . . . . . . . . . . . 17 (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) = โˆ…
3123, 24, 303eqtri 2763 . . . . . . . . . . . . . . . 16 (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )))) = โˆ…
3231uneq2i 4156 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช โˆ…)
33 un0 4386 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช โˆ…) = (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))
3432, 33eqtri 2759 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))
35 ssun2 4169 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
36 ssun2 4169 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
3735, 36sstri 3987 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
38 ssun2 4169 . . . . . . . . . . . . . . 15 (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
3937, 38sstri 3987 . . . . . . . . . . . . . 14 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
4034, 39eqsstri 4012 . . . . . . . . . . . . 13 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
4140sseli 3974 . . . . . . . . . . . 12 (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
4241imim1i 63 . . . . . . . . . . 11 ((((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
43426ralimi 3126 . . . . . . . . . 10 (โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
441, 43syl 17 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
4544, 5, 7mulsproplem11 27495 . . . . . . . 8 (๐œ‘ โ†’ (๐ท ยทs ๐ธ) โˆˆ No )
4631uneq2i 4156 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช โˆ…)
47 un0 4386 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช โˆ…) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ))
4846, 47eqtri 2759 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ))
49 ssun1 4168 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
50 ssun1 4168 . . . . . . . . . . . . . . . 16 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
5149, 50sstri 3987 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
5251, 38sstri 3987 . . . . . . . . . . . . . 14 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
5348, 52eqsstri 4012 . . . . . . . . . . . . 13 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
5453sseli 3974 . . . . . . . . . . . 12 (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
5554imim1i 63 . . . . . . . . . . 11 ((((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
56556ralimi 3126 . . . . . . . . . 10 (โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
571, 56syl 17 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
5857, 3, 7mulsproplem11 27495 . . . . . . . 8 (๐œ‘ โ†’ (๐ถ ยทs ๐ธ) โˆˆ No )
5945, 58subscld 27449 . . . . . . 7 (๐œ‘ โ†’ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) โˆˆ No )
6059adantr 481 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) โˆˆ No )
6144adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
625adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ท โˆˆ No )
63 simprr1 1221 . . . . . . . . . 10 ((( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ))
6463adantl 482 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ))
65 bdayelon 27204 . . . . . . . . . 10 ( bday โ€˜๐ธ) โˆˆ On
66 simprrl 779 . . . . . . . . . 10 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐‘ฅ โˆˆ No )
67 oldbday 27318 . . . . . . . . . 10 ((( bday โ€˜๐ธ) โˆˆ On โˆง ๐‘ฅ โˆˆ No ) โ†’ (๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ธ)) โ†” ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ)))
6865, 66, 67sylancr 587 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ธ)) โ†” ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ)))
6964, 68mpbird 256 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ธ)))
7061, 62, 69mulsproplem3 27487 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ท ยทs ๐‘ฅ) โˆˆ No )
7157adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
723adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ถ โˆˆ No )
7371, 72, 69mulsproplem3 27487 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ถ ยทs ๐‘ฅ) โˆˆ No )
7470, 73subscld 27449 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)) โˆˆ No )
7531uneq2i 4156 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช โˆ…)
76 un0 4386 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช โˆ…) = (( bday โ€˜๐ท) +no ( bday โ€˜๐น))
7775, 76eqtri 2759 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = (( bday โ€˜๐ท) +no ( bday โ€˜๐น))
78 ssun2 4169 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
7978, 50sstri 3987 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
8079, 38sstri 3987 . . . . . . . . . . . . . 14 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
8177, 80eqsstri 4012 . . . . . . . . . . . . 13 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
8281sseli 3974 . . . . . . . . . . . 12 (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
8382imim1i 63 . . . . . . . . . . 11 ((((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
84836ralimi 3126 . . . . . . . . . 10 (โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
851, 84syl 17 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
8685, 5, 9mulsproplem11 27495 . . . . . . . 8 (๐œ‘ โ†’ (๐ท ยทs ๐น) โˆˆ No )
8731uneq2i 4156 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช โˆ…)
88 un0 4386 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช โˆ…) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐น))
8987, 88eqtri 2759 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐น))
90 ssun1 4168 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
9190, 36sstri 3987 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
9291, 38sstri 3987 . . . . . . . . . . . . . 14 (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
9389, 92eqsstri 4012 . . . . . . . . . . . . 13 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
9493sseli 3974 . . . . . . . . . . . 12 (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
9594imim1i 63 . . . . . . . . . . 11 ((((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
96956ralimi 3126 . . . . . . . . . 10 (โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))) โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
971, 96syl 17 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘ โˆˆ No โˆ€๐‘‘ โˆˆ No โˆ€๐‘’ โˆˆ No โˆ€๐‘“ โˆˆ No (((( bday โ€˜๐‘Ž) +no ( bday โ€˜๐‘)) โˆช (((( bday โ€˜๐‘) +no ( bday โ€˜๐‘’)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘“))) โˆช ((( bday โ€˜๐‘) +no ( bday โ€˜๐‘“)) โˆช (( bday โ€˜๐‘‘) +no ( bday โ€˜๐‘’))))) โˆˆ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))))) โ†’ ((๐‘Ž ยทs ๐‘) โˆˆ No โˆง ((๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“) โ†’ ((๐‘ ยทs ๐‘“) -s (๐‘ ยทs ๐‘’)) <s ((๐‘‘ ยทs ๐‘“) -s (๐‘‘ ยทs ๐‘’))))))
9897, 3, 9mulsproplem11 27495 . . . . . . . 8 (๐œ‘ โ†’ (๐ถ ยทs ๐น) โˆˆ No )
9986, 98subscld 27449 . . . . . . 7 (๐œ‘ โ†’ ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โˆˆ No )
10099adantr 481 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โˆˆ No )
1011mulsproplemcbv 27484 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))))
102101adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))))
103 onelss 6395 . . . . . . . . . . . . . . . . . 18 (( bday โ€˜๐ธ) โˆˆ On โ†’ (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โ†’ ( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ธ)))
10465, 64, 103mpsyl 68 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ธ))
105 simprl 769 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐ธ) = ( bday โ€˜๐น))
106104, 105sseqtrd 4018 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐น))
107 bdayelon 27204 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐‘ฅ) โˆˆ On
108 bdayelon 27204 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐น) โˆˆ On
109 bdayelon 27204 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐ท) โˆˆ On
110 naddss2 8672 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐น) โˆˆ On โˆง ( bday โ€˜๐ท) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐น) โ†” (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
111107, 108, 109, 110mp3an 1461 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐น) โ†” (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
112106, 111sylib 217 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
113 unss2 4177 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
114112, 113syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
115 bdayelon 27204 . . . . . . . . . . . . . . . . 17 ( bday โ€˜๐ถ) โˆˆ On
116 naddss2 8672 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐น) โˆˆ On โˆง ( bday โ€˜๐ถ) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐น) โ†” (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐น))))
117107, 108, 115, 116mp3an 1461 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐น) โ†” (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)))
118106, 117sylib 217 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)))
119 unss1 4175 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
120118, 119syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
121 unss12 4178 . . . . . . . . . . . . . 14 ((((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆง ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โ†’ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
122114, 120, 121syl2anc 584 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
123 unss2 4177 . . . . . . . . . . . . 13 ((((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
124122, 123syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
125124sseld 3977 . . . . . . . . . . 11 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))))
126125imim1d 82 . . . . . . . . . 10 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))) โ†’ (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜)))))))
127126ralimd6v 3207 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜)))))))
128102, 127mpd 15 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))))
1297adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ธ โˆˆ No )
13011adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ถ <s ๐ท)
131 simprr2 1222 . . . . . . . . 9 ((( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))) โ†’ ๐ธ <s ๐‘ฅ)
132131adantl 482 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐ธ <s ๐‘ฅ)
13364olcd 872 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐‘ฅ) โˆจ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ)))
134128, 72, 62, 129, 66, 130, 132, 133mulsproplem13 27497 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ถ ยทs ๐‘ฅ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐‘ฅ) -s (๐ท ยทs ๐ธ)))
13545adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ท ยทs ๐ธ) โˆˆ No )
13658adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ถ ยทs ๐ธ) โˆˆ No )
137135, 70, 136, 73sltsubsub3bd 27466 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)) โ†” ((๐ถ ยทs ๐‘ฅ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐‘ฅ) -s (๐ท ยทs ๐ธ))))
138134, 137mpbird 256 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)))
139 naddss2 8672 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐ธ) โˆˆ On โˆง ( bday โ€˜๐ถ) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ธ) โ†” (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ))))
140107, 65, 115, 139mp3an 1461 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ธ) โ†” (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)))
141104, 140sylib 217 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)))
142 unss1 4175 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
143141, 142syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
144 naddss2 8672 . . . . . . . . . . . . . . . . 17 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐ธ) โˆˆ On โˆง ( bday โ€˜๐ท) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ธ) โ†” (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
145107, 65, 109, 144mp3an 1461 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ธ) โ†” (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
146104, 145sylib 217 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
147 unss2 4177 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
148146, 147syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
149 unss12 4178 . . . . . . . . . . . . . 14 ((((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆง ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โ†’ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
150143, 148, 149syl2anc 584 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
151 unss2 4177 . . . . . . . . . . . . 13 ((((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ)))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))) โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
152150, 151syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
153152sseld 3977 . . . . . . . . . . 11 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โ†’ ((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))))
154153imim1d 82 . . . . . . . . . 10 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))) โ†’ (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜)))))))
155154ralimd6v 3207 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜)))))))
156102, 155mpd 15 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ โˆ€๐‘” โˆˆ No โˆ€โ„Ž โˆˆ No โˆ€๐‘– โˆˆ No โˆ€๐‘— โˆˆ No โˆ€๐‘˜ โˆˆ No โˆ€๐‘™ โˆˆ No (((( bday โ€˜๐‘”) +no ( bday โ€˜โ„Ž)) โˆช (((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘˜)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘™))) โˆช ((( bday โ€˜๐‘–) +no ( bday โ€˜๐‘™)) โˆช (( bday โ€˜๐‘—) +no ( bday โ€˜๐‘˜))))) โˆˆ ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐‘ฅ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐‘ฅ))))) โ†’ ((๐‘” ยทs โ„Ž) โˆˆ No โˆง ((๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™) โ†’ ((๐‘– ยทs ๐‘™) -s (๐‘– ยทs ๐‘˜)) <s ((๐‘— ยทs ๐‘™) -s (๐‘— ยทs ๐‘˜))))))
1579adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐น โˆˆ No )
158 simprr3 1223 . . . . . . . . 9 ((( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))) โ†’ ๐‘ฅ <s ๐น)
159158adantl 482 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ๐‘ฅ <s ๐น)
16064, 105eleqtrd 2834 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐น))
161160orcd 871 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐‘ฅ)))
162156, 72, 62, 66, 157, 130, 159, 161mulsproplem13 27497 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐‘ฅ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐‘ฅ)))
16386adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ท ยทs ๐น) โˆˆ No )
16498adantr 481 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (๐ถ ยทs ๐น) โˆˆ No )
16570, 163, 73, 164sltsubsub3bd 27466 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ†” ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐‘ฅ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐‘ฅ))))
166162, 165mpbird 256 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐‘ฅ) -s (๐ถ ยทs ๐‘ฅ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)))
16760, 74, 100, 138, 166slttrd 27189 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)))
16845, 86, 58, 98sltsubsub3bd 27466 . . . . . 6 (๐œ‘ โ†’ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ†” ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))))
169168adantr 481 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ (((๐ท ยทs ๐ธ) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ถ ยทs ๐น)) โ†” ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ))))
170167, 169mpbid 231 . . . 4 ((๐œ‘ โˆง (( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น)))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
171170anassrs 468 . . 3 (((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ธ) โˆง ๐ธ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐น))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
17222, 171rexlimddv 3160 . 2 ((๐œ‘ โˆง ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
17365onordi 6464 . . . . 5 Ord ( bday โ€˜๐ธ)
174108onordi 6464 . . . . 5 Ord ( bday โ€˜๐น)
175 ordtri3or 6385 . . . . 5 ((Ord ( bday โ€˜๐ธ) โˆง Ord ( bday โ€˜๐น)) โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
176173, 174, 175mp2an 690 . . . 4 (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ))
177 df-3or 1088 . . . . 5 ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โ†” ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
178 or32 924 . . . . 5 (((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โ†” ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)))
179177, 178bitri 274 . . . 4 ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โ†” ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)))
180176, 179mpbi 229 . . 3 ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น))
181180a1i 11 . 2 (๐œ‘ โ†’ ((( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)) โˆจ ( bday โ€˜๐ธ) = ( bday โ€˜๐น)))
18216, 172, 181mpjaodan 957 1 (๐œ‘ โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆจ w3o 1086   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3060  โˆƒwrex 3069   โˆช cun 3942   โŠ† wss 3944  โˆ…c0 4318   class class class wbr 5141  Ord word 6352  Oncon0 6353  โ€˜cfv 6532  (class class class)co 7393   +no cnadd 8647   No csur 27070   <s cslt 27071   bday cbday 27072   0s c0s 27249   O cold 27261   -s csubs 27411   ยทs cmuls 27476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-ot 4631  df-uni 4902  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-1st 7957  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-1o 8448  df-2o 8449  df-nadd 8648  df-no 27073  df-slt 27074  df-bday 27075  df-sle 27175  df-sslt 27209  df-scut 27211  df-0s 27251  df-made 27265  df-old 27266  df-left 27268  df-right 27269  df-norec 27338  df-norec2 27349  df-adds 27360  df-negs 27412  df-subs 27413  df-muls 27477
This theorem is referenced by:  mulsprop  27499
  Copyright terms: Public domain W3C validator