Metamath Proof Explorer

Theorem mulsproplemcbv

Description: Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypothesis 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 ๐‘’ ) ) ) ) ) )
Assertion mulsproplemcbv ( ๐œ‘ โ†’ โˆ€ ๐‘” โˆˆ 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 ๐‘˜ ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ๐‘’ ) ) ) ) ) )
2 fveq2 โŠข ( ๐‘Ž = ๐‘” โ†’ ( bday โ€˜ ๐‘Ž ) = ( bday โ€˜ ๐‘” ) )
3 2 oveq1d โŠข ( ๐‘Ž = ๐‘” โ†’ ( ( bday โ€˜ ๐‘Ž ) +no ( bday โ€˜ ๐‘ ) ) = ( ( bday โ€˜ ๐‘” ) +no ( bday โ€˜ ๐‘ ) ) )
4 3 uneq1d โŠข ( ๐‘Ž = ๐‘” โ†’ ( ( ( 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 โ€˜ ๐‘’ ) ) ) ) ) )
5 4 eleq1d โŠข ( ๐‘Ž = ๐‘” โ†’ ( ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) ) )
6 oveq1 โŠข ( ๐‘Ž = ๐‘” โ†’ ( ๐‘Ž ยทs ๐‘ ) = ( ๐‘” ยทs ๐‘ ) )
7 6 eleq1d โŠข ( ๐‘Ž = ๐‘” โ†’ ( ( ๐‘Ž ยทs ๐‘ ) โˆˆ No โ†” ( ๐‘” ยทs ๐‘ ) โˆˆ No ) )
8 7 anbi1d โŠข ( ๐‘Ž = ๐‘” โ†’ ( ( ( ๐‘Ž ยทs ๐‘ ) โˆˆ No โˆง ( ( ๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘ ยทs ๐‘“ ) -s ( ๐‘ ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) ) โ†” ( ( ๐‘” ยทs ๐‘ ) โˆˆ No โˆง ( ( ๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘ ยทs ๐‘“ ) -s ( ๐‘ ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) ) ) )
9 5 8 imbi12d โŠข ( ๐‘Ž = ๐‘” โ†’ ( ( ( ( ( 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 ๐‘’ ) ) ) ) ) ) )
10 fveq2 โŠข ( ๐‘ = โ„Ž โ†’ ( bday โ€˜ ๐‘ ) = ( bday โ€˜ โ„Ž ) )
11 10 oveq2d โŠข ( ๐‘ = โ„Ž โ†’ ( ( bday โ€˜ ๐‘” ) +no ( bday โ€˜ ๐‘ ) ) = ( ( bday โ€˜ ๐‘” ) +no ( bday โ€˜ โ„Ž ) ) )
12 11 uneq1d โŠข ( ๐‘ = โ„Ž โ†’ ( ( ( 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 โ€˜ ๐‘’ ) ) ) ) ) )
13 12 eleq1d โŠข ( ๐‘ = โ„Ž โ†’ ( ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) ) )
14 oveq2 โŠข ( ๐‘ = โ„Ž โ†’ ( ๐‘” ยทs ๐‘ ) = ( ๐‘” ยทs โ„Ž ) )
15 14 eleq1d โŠข ( ๐‘ = โ„Ž โ†’ ( ( ๐‘” ยทs ๐‘ ) โˆˆ No โ†” ( ๐‘” ยทs โ„Ž ) โˆˆ No ) )
16 15 anbi1d โŠข ( ๐‘ = โ„Ž โ†’ ( ( ( ๐‘” ยทs ๐‘ ) โˆˆ No โˆง ( ( ๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘ ยทs ๐‘“ ) -s ( ๐‘ ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) ) โ†” ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘ ยทs ๐‘“ ) -s ( ๐‘ ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) ) ) )
17 13 16 imbi12d โŠข ( ๐‘ = โ„Ž โ†’ ( ( ( ( ( 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 ๐‘’ ) ) ) ) ) ) )
18 fveq2 โŠข ( ๐‘ = ๐‘– โ†’ ( bday โ€˜ ๐‘ ) = ( bday โ€˜ ๐‘– ) )
19 18 oveq1d โŠข ( ๐‘ = ๐‘– โ†’ ( ( bday โ€˜ ๐‘ ) +no ( bday โ€˜ ๐‘’ ) ) = ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) )
20 19 uneq1d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( bday โ€˜ ๐‘ ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘“ ) ) ) = ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘“ ) ) ) )
21 18 oveq1d โŠข ( ๐‘ = ๐‘– โ†’ ( ( bday โ€˜ ๐‘ ) +no ( bday โ€˜ ๐‘“ ) ) = ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) )
22 21 uneq1d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( bday โ€˜ ๐‘ ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘’ ) ) ) = ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘’ ) ) ) )
23 20 22 uneq12d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( ( bday โ€˜ ๐‘ ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘“ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘ ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘’ ) ) ) ) = ( ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘“ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘’ ) ) ) ) )
24 23 uneq2d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( 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 โ€˜ ๐‘’ ) ) ) ) ) )
25 24 eleq1d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) ) )
26 breq1 โŠข ( ๐‘ = ๐‘– โ†’ ( ๐‘ <s ๐‘‘ โ†” ๐‘– <s ๐‘‘ ) )
27 26 anbi1d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†” ( ๐‘– <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) ) )
28 oveq1 โŠข ( ๐‘ = ๐‘– โ†’ ( ๐‘ ยทs ๐‘“ ) = ( ๐‘– ยทs ๐‘“ ) )
29 oveq1 โŠข ( ๐‘ = ๐‘– โ†’ ( ๐‘ ยทs ๐‘’ ) = ( ๐‘– ยทs ๐‘’ ) )
30 28 29 oveq12d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ๐‘ ยทs ๐‘“ ) -s ( ๐‘ ยทs ๐‘’ ) ) = ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) )
31 30 breq1d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( ๐‘ ยทs ๐‘“ ) -s ( ๐‘ ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) โ†” ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) )
32 27 31 imbi12d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( ๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘ ยทs ๐‘“ ) -s ( ๐‘ ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) โ†” ( ( ๐‘– <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) ) )
33 32 anbi2d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘ <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘ ยทs ๐‘“ ) -s ( ๐‘ ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) ) โ†” ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘– <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) ) ) )
34 25 33 imbi12d โŠข ( ๐‘ = ๐‘– โ†’ ( ( ( ( ( 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 ๐‘’ ) ) ) ) ) ) )
35 fveq2 โŠข ( ๐‘‘ = ๐‘— โ†’ ( bday โ€˜ ๐‘‘ ) = ( bday โ€˜ ๐‘— ) )
36 35 oveq1d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘“ ) ) = ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) )
37 36 uneq2d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘“ ) ) ) = ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) ) )
38 35 oveq1d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘’ ) ) = ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘’ ) ) )
39 38 uneq2d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘’ ) ) ) = ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘’ ) ) ) )
40 37 39 uneq12d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘“ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘‘ ) +no ( bday โ€˜ ๐‘’ ) ) ) ) = ( ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘’ ) ) ) ) )
41 40 uneq2d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( 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 โ€˜ ๐‘’ ) ) ) ) ) )
42 41 eleq1d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) ) )
43 breq2 โŠข ( ๐‘‘ = ๐‘— โ†’ ( ๐‘– <s ๐‘‘ โ†” ๐‘– <s ๐‘— ) )
44 43 anbi1d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ๐‘– <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†” ( ๐‘– <s ๐‘— โˆง ๐‘’ <s ๐‘“ ) ) )
45 oveq1 โŠข ( ๐‘‘ = ๐‘— โ†’ ( ๐‘‘ ยทs ๐‘“ ) = ( ๐‘— ยทs ๐‘“ ) )
46 oveq1 โŠข ( ๐‘‘ = ๐‘— โ†’ ( ๐‘‘ ยทs ๐‘’ ) = ( ๐‘— ยทs ๐‘’ ) )
47 45 46 oveq12d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) = ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘’ ) ) )
48 47 breq2d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) โ†” ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘’ ) ) ) )
49 44 48 imbi12d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( ๐‘– <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) โ†” ( ( ๐‘– <s ๐‘— โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘’ ) ) ) ) )
50 49 anbi2d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘– <s ๐‘‘ โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘‘ ยทs ๐‘“ ) -s ( ๐‘‘ ยทs ๐‘’ ) ) ) ) โ†” ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘– <s ๐‘— โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘’ ) ) ) ) ) )
51 42 50 imbi12d โŠข ( ๐‘‘ = ๐‘— โ†’ ( ( ( ( ( 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 ๐‘’ ) ) ) ) ) ) )
52 fveq2 โŠข ( ๐‘’ = ๐‘˜ โ†’ ( bday โ€˜ ๐‘’ ) = ( bday โ€˜ ๐‘˜ ) )
53 52 oveq2d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) = ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘˜ ) ) )
54 53 uneq1d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) ) = ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘˜ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) ) )
55 52 oveq2d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘’ ) ) = ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘˜ ) ) )
56 55 uneq2d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘’ ) ) ) = ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘˜ ) ) ) )
57 54 56 uneq12d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘’ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘’ ) ) ) ) = ( ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘˜ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘˜ ) ) ) ) )
58 57 uneq2d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( 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 โ€˜ ๐‘˜ ) ) ) ) ) )
59 58 eleq1d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) ) )
60 breq1 โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ๐‘’ <s ๐‘“ โ†” ๐‘˜ <s ๐‘“ ) )
61 60 anbi2d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ๐‘– <s ๐‘— โˆง ๐‘’ <s ๐‘“ ) โ†” ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘“ ) ) )
62 oveq2 โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ๐‘– ยทs ๐‘’ ) = ( ๐‘– ยทs ๐‘˜ ) )
63 62 oveq2d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) = ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘˜ ) ) )
64 oveq2 โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ๐‘— ยทs ๐‘’ ) = ( ๐‘— ยทs ๐‘˜ ) )
65 64 oveq2d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘’ ) ) = ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘˜ ) ) )
66 63 65 breq12d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘’ ) ) โ†” ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘˜ ) ) ) )
67 61 66 imbi12d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( ๐‘– <s ๐‘— โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘’ ) ) ) โ†” ( ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘˜ ) ) ) ) )
68 67 anbi2d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘– <s ๐‘— โˆง ๐‘’ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘’ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘’ ) ) ) ) โ†” ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘˜ ) ) ) ) ) )
69 59 68 imbi12d โŠข ( ๐‘’ = ๐‘˜ โ†’ ( ( ( ( ( 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 ๐‘˜ ) ) ) ) ) ) )
70 fveq2 โŠข ( ๐‘“ = ๐‘™ โ†’ ( bday โ€˜ ๐‘“ ) = ( bday โ€˜ ๐‘™ ) )
71 70 oveq2d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) = ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘™ ) ) )
72 71 uneq2d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘˜ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) ) = ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘˜ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘™ ) ) ) )
73 70 oveq2d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) = ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘™ ) ) )
74 73 uneq1d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘˜ ) ) ) = ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘™ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘˜ ) ) ) )
75 72 74 uneq12d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘˜ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘“ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘“ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘˜ ) ) ) ) = ( ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘˜ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘™ ) ) ) โˆช ( ( ( bday โ€˜ ๐‘– ) +no ( bday โ€˜ ๐‘™ ) ) โˆช ( ( bday โ€˜ ๐‘— ) +no ( bday โ€˜ ๐‘˜ ) ) ) ) )
76 75 uneq2d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( 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 โ€˜ ๐‘˜ ) ) ) ) ) )
77 76 eleq1d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( ( 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 โ€˜ ๐ธ ) ) ) ) ) ) )
78 breq2 โŠข ( ๐‘“ = ๐‘™ โ†’ ( ๐‘˜ <s ๐‘“ โ†” ๐‘˜ <s ๐‘™ ) )
79 78 anbi2d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘“ ) โ†” ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™ ) ) )
80 oveq2 โŠข ( ๐‘“ = ๐‘™ โ†’ ( ๐‘– ยทs ๐‘“ ) = ( ๐‘– ยทs ๐‘™ ) )
81 80 oveq1d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘˜ ) ) = ( ( ๐‘– ยทs ๐‘™ ) -s ( ๐‘– ยทs ๐‘˜ ) ) )
82 oveq2 โŠข ( ๐‘“ = ๐‘™ โ†’ ( ๐‘— ยทs ๐‘“ ) = ( ๐‘— ยทs ๐‘™ ) )
83 82 oveq1d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘˜ ) ) = ( ( ๐‘— ยทs ๐‘™ ) -s ( ๐‘— ยทs ๐‘˜ ) ) )
84 81 83 breq12d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘˜ ) ) โ†” ( ( ๐‘– ยทs ๐‘™ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘™ ) -s ( ๐‘— ยทs ๐‘˜ ) ) ) )
85 79 84 imbi12d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘˜ ) ) ) โ†” ( ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™ ) โ†’ ( ( ๐‘– ยทs ๐‘™ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘™ ) -s ( ๐‘— ยทs ๐‘˜ ) ) ) ) )
86 85 anbi2d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘“ ) โ†’ ( ( ๐‘– ยทs ๐‘“ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘“ ) -s ( ๐‘— ยทs ๐‘˜ ) ) ) ) โ†” ( ( ๐‘” ยทs โ„Ž ) โˆˆ No โˆง ( ( ๐‘– <s ๐‘— โˆง ๐‘˜ <s ๐‘™ ) โ†’ ( ( ๐‘– ยทs ๐‘™ ) -s ( ๐‘– ยทs ๐‘˜ ) ) <s ( ( ๐‘— ยทs ๐‘™ ) -s ( ๐‘— ยทs ๐‘˜ ) ) ) ) ) )
87 77 86 imbi12d โŠข ( ๐‘“ = ๐‘™ โ†’ ( ( ( ( ( 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 ๐‘˜ ) ) ) ) ) ) )
88 9 17 34 51 69 87 cbvral6vw โŠข ( โˆ€ ๐‘Ž โˆˆ 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 ๐‘˜ ) ) ) ) ) )
89 1 88 sylib โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘” โˆˆ 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 ๐‘˜ ) ) ) ) ) )