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

Theorem mulsproplem13 27497
Description: Lemma for surreal multiplication. Remove the restriction on ๐ถ and ๐ท from mulsproplem12 27496. (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 ๐น)
mulsproplem13.1 (๐œ‘ โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
Assertion
Ref Expression
mulsproplem13 (๐œ‘ โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ต,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ถ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ท,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐ธ,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“   ๐น,๐‘Ž,๐‘,๐‘,๐‘‘,๐‘’,๐‘“
Allowed substitution hints:   ๐œ‘(๐‘’,๐‘“,๐‘Ž,๐‘,๐‘,๐‘‘)

Proof of Theorem mulsproplem13
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 โ€˜๐ถ)))
16 mulsproplem13.1 . . . 4 (๐œ‘ โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
1716adantr 481 . . 3 ((๐œ‘ โˆง (( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ))) โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
182, 4, 6, 8, 10, 12, 14, 15, 17mulsproplem12 27496 . 2 ((๐œ‘ โˆง (( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
193adantr 481 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โ†’ ๐ถ โˆˆ No )
205adantr 481 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โ†’ ๐ท โˆˆ No )
21 simpr 485 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โ†’ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท))
2211adantr 481 . . . 4 ((๐œ‘ โˆง ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โ†’ ๐ถ <s ๐ท)
23 nodense 27122 . . . 4 (((๐ถ โˆˆ No โˆง ๐ท โˆˆ No ) โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง ๐ถ <s ๐ท)) โ†’ โˆƒ๐‘ฅ โˆˆ No (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท))
2419, 20, 21, 22, 23syl22anc 837 . . 3 ((๐œ‘ โˆง ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โ†’ โˆƒ๐‘ฅ โˆˆ No (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท))
25 unidm 4148 . . . . . . . . . . . . . . . 16 (((( 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 )))
26 unidm 4148 . . . . . . . . . . . . . . . 16 ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) = (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))
27 bday0s 27255 . . . . . . . . . . . . . . . . . 18 ( bday โ€˜ 0s ) = โˆ…
2827, 27oveq12i 7405 . . . . . . . . . . . . . . . . 17 (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) = (โˆ… +no โˆ…)
29 0elon 6407 . . . . . . . . . . . . . . . . . 18 โˆ… โˆˆ On
30 naddrid 8665 . . . . . . . . . . . . . . . . . 18 (โˆ… โˆˆ On โ†’ (โˆ… +no โˆ…) = โˆ…)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . 17 (โˆ… +no โˆ…) = โˆ…
3228, 31eqtri 2759 . . . . . . . . . . . . . . . 16 (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) = โˆ…
3325, 26, 323eqtri 2763 . . . . . . . . . . . . . . 15 (((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s ))) โˆช ((( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )) โˆช (( bday โ€˜ 0s ) +no ( bday โ€˜ 0s )))) = โˆ…
3433uneq2i 4156 . . . . . . . . . . . . . 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 un0 4386 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช โˆ…) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐น))
3634, 35eqtri 2759 . . . . . . . . . . . . 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 โ€˜๐น))
37 ssun1 4168 . . . . . . . . . . . . . . 15 (( 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 โ€˜๐ธ))))
3937, 38sstri 3987 . . . . . . . . . . . . . 14 (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
40 ssun2 4169 . . . . . . . . . . . . . 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 โ€˜๐ธ)))))
4139, 40sstri 3987 . . . . . . . . . . . . 13 (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
4236, 41eqsstri 4012 . . . . . . . . . . . 12 ((( 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 โ€˜๐ธ)))))
4342sseli 3974 . . . . . . . . . . 11 (((( 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 โ€˜๐ธ))))))
4443imim1i 63 . . . . . . . . . 10 ((((( 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 ๐‘’))))))
45446ralimi 3126 . . . . . . . . 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 โ€˜๐ถ) +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 ๐‘’))))))
461, 45syl 17 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ 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 ๐‘’))))))
4746, 3, 9mulsproplem11 27495 . . . . . . 7 (๐œ‘ โ†’ (๐ถ ยทs ๐น) โˆˆ No )
4833uneq2i 4156 . . . . . . . . . . . . . 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 un0 4386 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช โˆ…) = (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ))
5048, 49eqtri 2759 . . . . . . . . . . . . 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 โ€˜๐ธ))
51 ssun1 4168 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
52 ssun1 4168 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
5351, 52sstri 3987 . . . . . . . . . . . . . 14 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
5453, 40sstri 3987 . . . . . . . . . . . . 13 (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
5550, 54eqsstri 4012 . . . . . . . . . . . 12 ((( 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 โ€˜๐ธ)))))
5655sseli 3974 . . . . . . . . . . 11 (((( 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 โ€˜๐ธ))))))
5756imim1i 63 . . . . . . . . . 10 ((((( 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 ๐‘’))))))
58576ralimi 3126 . . . . . . . . 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 โ€˜๐ถ) +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 ๐‘’))))))
591, 58syl 17 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ 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 ๐‘’))))))
6059, 3, 7mulsproplem11 27495 . . . . . . 7 (๐œ‘ โ†’ (๐ถ ยทs ๐ธ) โˆˆ No )
6147, 60subscld 27449 . . . . . 6 (๐œ‘ โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) โˆˆ No )
6261adantr 481 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) โˆˆ No )
6346adantr 481 . . . . . . 7 ((๐œ‘ โˆง (( 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 ๐‘’))))))
64 simprr1 1221 . . . . . . . . 9 ((( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ))
6564adantl 482 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ))
66 bdayelon 27204 . . . . . . . . 9 ( bday โ€˜๐ถ) โˆˆ On
67 simprrl 779 . . . . . . . . 9 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐‘ฅ โˆˆ No )
68 oldbday 27318 . . . . . . . . 9 ((( bday โ€˜๐ถ) โˆˆ On โˆง ๐‘ฅ โˆˆ No ) โ†’ (๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ถ)) โ†” ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ)))
6966, 67, 68sylancr 587 . . . . . . . 8 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ถ)) โ†” ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ)))
7065, 69mpbird 256 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐‘ฅ โˆˆ ( O โ€˜( bday โ€˜๐ถ)))
719adantr 481 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐น โˆˆ No )
7263, 70, 71mulsproplem2 27486 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (๐‘ฅ ยทs ๐น) โˆˆ No )
7359adantr 481 . . . . . . 7 ((๐œ‘ โˆง (( 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 ๐‘’))))))
747adantr 481 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐ธ โˆˆ No )
7573, 70, 74mulsproplem2 27486 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (๐‘ฅ ยทs ๐ธ) โˆˆ No )
7672, 75subscld 27449 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((๐‘ฅ ยทs ๐น) -s (๐‘ฅ ยทs ๐ธ)) โˆˆ No )
7733uneq2i 4156 . . . . . . . . . . . . . 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 un0 4386 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โˆช โˆ…) = (( bday โ€˜๐ท) +no ( bday โ€˜๐น))
7977, 78eqtri 2759 . . . . . . . . . . . . 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 โ€˜๐น))
80 ssun2 4169 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
8180, 52sstri 3987 . . . . . . . . . . . . . 14 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
8281, 40sstri 3987 . . . . . . . . . . . . 13 (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
8379, 82eqsstri 4012 . . . . . . . . . . . 12 ((( 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 โ€˜๐ธ)))))
8483sseli 3974 . . . . . . . . . . 11 (((( 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 โ€˜๐ธ))))))
8584imim1i 63 . . . . . . . . . 10 ((((( 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 ๐‘’))))))
86856ralimi 3126 . . . . . . . . 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 โ€˜๐ถ) +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 ๐‘’))))))
871, 86syl 17 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ 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 ๐‘’))))))
8887, 5, 9mulsproplem11 27495 . . . . . . 7 (๐œ‘ โ†’ (๐ท ยทs ๐น) โˆˆ No )
8933uneq2i 4156 . . . . . . . . . . . . . 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 un0 4386 . . . . . . . . . . . . . 14 ((( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โˆช โˆ…) = (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))
9189, 90eqtri 2759 . . . . . . . . . . . . 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 โ€˜๐ธ))
92 ssun2 4169 . . . . . . . . . . . . . . 15 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
9392, 38sstri 3987 . . . . . . . . . . . . . 14 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โŠ† (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
9493, 40sstri 3987 . . . . . . . . . . . . 13 (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))))
9591, 94eqsstri 4012 . . . . . . . . . . . 12 ((( 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 โ€˜๐ธ)))))
9695sseli 3974 . . . . . . . . . . 11 (((( 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 โ€˜๐ธ))))))
9796imim1i 63 . . . . . . . . . 10 ((((( 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 ๐‘’))))))
98976ralimi 3126 . . . . . . . . 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 โ€˜๐ถ) +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 ๐‘’))))))
991, 98syl 17 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ 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 ๐‘’))))))
10099, 5, 7mulsproplem11 27495 . . . . . . 7 (๐œ‘ โ†’ (๐ท ยทs ๐ธ) โˆˆ No )
10188, 100subscld 27449 . . . . . 6 (๐œ‘ โ†’ ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)) โˆˆ No )
102101adantr 481 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)) โˆˆ No )
1031mulsproplemcbv 27484 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘” โˆˆ 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 ๐‘˜))))))
104103adantr 481 . . . . . . 7 ((๐œ‘ โˆง (( 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 ๐‘˜))))))
105 onelss 6395 . . . . . . . . . . . . . . . 16 (( bday โ€˜๐ถ) โˆˆ On โ†’ (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โ†’ ( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ถ)))
10666, 65, 105mpsyl 68 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ถ))
107 simprl 769 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท))
108106, 107sseqtrd 4018 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ท))
109 bdayelon 27204 . . . . . . . . . . . . . . 15 ( bday โ€˜๐‘ฅ) โˆˆ On
110 bdayelon 27204 . . . . . . . . . . . . . . 15 ( bday โ€˜๐ท) โˆˆ On
111 bdayelon 27204 . . . . . . . . . . . . . . 15 ( bday โ€˜๐น) โˆˆ On
112 naddss1 8671 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐ท) โˆˆ On โˆง ( bday โ€˜๐น) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ท) โ†” (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
113109, 110, 111, 112mp3an 1461 . . . . . . . . . . . . . 14 (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ท) โ†” (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
114108, 113sylib 217 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐น)))
115 unss2 4177 . . . . . . . . . . . . 13 ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐น)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
116114, 115syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
117 bdayelon 27204 . . . . . . . . . . . . . . 15 ( bday โ€˜๐ธ) โˆˆ On
118 naddss1 8671 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐ท) โˆˆ On โˆง ( bday โ€˜๐ธ) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ท) โ†” (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
119109, 110, 117, 118mp3an 1461 . . . . . . . . . . . . . 14 (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ท) โ†” (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
120108, 119sylib 217 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)))
121 unss2 4177 . . . . . . . . . . . . 13 ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โŠ† (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ)) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
122120, 121syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
123 unss12 4178 . . . . . . . . . . . 12 ((((( 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 โ€˜๐ธ)))))
124116, 122, 123syl2anc 584 . . . . . . . . . . 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 โ€˜๐ธ)))))
125 unss2 4177 . . . . . . . . . . 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 โ€˜๐ธ)) โˆช (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
126124, 125syl 17 . . . . . . . . . 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 โ€˜๐ธ))))))
127126sseld 3977 . . . . . . . . 9 ((๐œ‘ โˆง (( 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 โ€˜๐ธ)))))))
128127imim1d 82 . . . . . . . 8 ((๐œ‘ โˆง (( 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 ๐‘˜)))))))
129128ralimd6v 3207 . . . . . . 7 ((๐œ‘ โˆง (( 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 ๐‘˜)))))))
130104, 129mpd 15 . . . . . 6 ((๐œ‘ โˆง (( 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 ๐‘˜))))))
1313adantr 481 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐ถ โˆˆ No )
132 simprr2 1222 . . . . . . 7 ((( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท))) โ†’ ๐ถ <s ๐‘ฅ)
133132adantl 482 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐ถ <s ๐‘ฅ)
13413adantr 481 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐ธ <s ๐น)
13565olcd 872 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐‘ฅ) โˆจ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ)))
13616adantr 481 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (( bday โ€˜๐ธ) โˆˆ ( bday โ€˜๐น) โˆจ ( bday โ€˜๐น) โˆˆ ( bday โ€˜๐ธ)))
137130, 131, 67, 74, 71, 133, 134, 135, 136mulsproplem12 27496 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐‘ฅ ยทs ๐น) -s (๐‘ฅ ยทs ๐ธ)))
138 naddss1 8671 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐ถ) โˆˆ On โˆง ( bday โ€˜๐ธ) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ถ) โ†” (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ))))
139109, 66, 117, 138mp3an 1461 . . . . . . . . . . . . . 14 (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ถ) โ†” (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)))
140106, 139sylib 217 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)))
141 unss1 4175 . . . . . . . . . . . . 13 ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โ†’ ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
142140, 141syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))))
143 naddss1 8671 . . . . . . . . . . . . . . 15 ((( bday โ€˜๐‘ฅ) โˆˆ On โˆง ( bday โ€˜๐ถ) โˆˆ On โˆง ( bday โ€˜๐น) โˆˆ On) โ†’ (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ถ) โ†” (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐น))))
144109, 66, 111, 143mp3an 1461 . . . . . . . . . . . . . 14 (( bday โ€˜๐‘ฅ) โŠ† ( bday โ€˜๐ถ) โ†” (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)))
145106, 144sylib 217 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)))
146 unss1 4175 . . . . . . . . . . . . 13 ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โŠ† (( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โ†’ ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
147145, 146syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))) โŠ† ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))
148 unss12 4178 . . . . . . . . . . . 12 ((((( 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 โ€˜๐ธ)))))
149142, 147, 148syl2anc 584 . . . . . . . . . . 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 โ€˜๐ธ)))))
150 unss2 4177 . . . . . . . . . . 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 โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐‘ฅ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))) โŠ† ((( bday โ€˜๐ด) +no ( bday โ€˜๐ต)) โˆช (((( bday โ€˜๐ถ) +no ( bday โ€˜๐ธ)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐น))) โˆช ((( bday โ€˜๐ถ) +no ( bday โ€˜๐น)) โˆช (( bday โ€˜๐ท) +no ( bday โ€˜๐ธ))))))
151149, 150syl 17 . . . . . . . . . 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 โ€˜๐ธ))))))
152151sseld 3977 . . . . . . . . 9 ((๐œ‘ โˆง (( 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 โ€˜๐ธ)))))))
153152imim1d 82 . . . . . . . 8 ((๐œ‘ โˆง (( 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 ๐‘˜)))))))
154153ralimd6v 3207 . . . . . . 7 ((๐œ‘ โˆง (( 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 ๐‘˜)))))))
155104, 154mpd 15 . . . . . 6 ((๐œ‘ โˆง (( 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 ๐‘˜))))))
1565adantr 481 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐ท โˆˆ No )
157 simprr3 1223 . . . . . . 7 ((( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท))) โ†’ ๐‘ฅ <s ๐ท)
158157adantl 482 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ๐‘ฅ <s ๐ท)
15965, 107eleqtrd 2834 . . . . . . 7 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ท))
160159orcd 871 . . . . . 6 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐‘ฅ)))
161155, 67, 156, 74, 71, 158, 134, 160, 136mulsproplem12 27496 . . . . 5 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((๐‘ฅ ยทs ๐น) -s (๐‘ฅ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
16262, 76, 102, 137, 161slttrd 27189 . . . 4 ((๐œ‘ โˆง (( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท)))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
163162anassrs 468 . . 3 (((๐œ‘ โˆง ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โˆง (๐‘ฅ โˆˆ No โˆง (( bday โ€˜๐‘ฅ) โˆˆ ( bday โ€˜๐ถ) โˆง ๐ถ <s ๐‘ฅ โˆง ๐‘ฅ <s ๐ท))) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
16424, 163rexlimddv 3160 . 2 ((๐œ‘ โˆง ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โ†’ ((๐ถ ยทs ๐น) -s (๐ถ ยทs ๐ธ)) <s ((๐ท ยทs ๐น) -s (๐ท ยทs ๐ธ)))
16566onordi 6464 . . . . 5 Ord ( bday โ€˜๐ถ)
166110onordi 6464 . . . . 5 Ord ( bday โ€˜๐ท)
167 ordtri3or 6385 . . . . 5 ((Ord ( bday โ€˜๐ถ) โˆง Ord ( bday โ€˜๐ท)) โ†’ (( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)))
168165, 166, 167mp2an 690 . . . 4 (( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ))
169 df-3or 1088 . . . . 5 ((( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)) โ†” ((( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)))
170 or32 924 . . . . 5 (((( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)) โ†” ((( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)))
171169, 170bitri 274 . . . 4 ((( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)) โ†” ((( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)))
172168, 171mpbi 229 . . 3 ((( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท))
173172a1i 11 . 2 (๐œ‘ โ†’ ((( bday โ€˜๐ถ) โˆˆ ( bday โ€˜๐ท) โˆจ ( bday โ€˜๐ท) โˆˆ ( bday โ€˜๐ถ)) โˆจ ( bday โ€˜๐ถ) = ( bday โ€˜๐ท)))
17418, 164, 173mpjaodan 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:  mulsproplem14  27498
  Copyright terms: Public domain W3C validator