MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsprop Structured version   Visualization version   GIF version
Theorem mulsprop 28509
Description: Surreals are closed under multiplication and obey a particular ordering law. Theorem 3.4 of [Gonshor] p. 17. (Contributed by Scott Fenton, 5-Mar-2025.)
Assertion
Ref Expression
mulsprop (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ (𝐸 ∈ No ∧ 𝐹 ∈ No )) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
Proof of Theorem mulsprop
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑖 𝑗 𝑘 𝑙 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bdayon 28131 . . . . 5 ( bday ‘𝐴) ∈ On
2 bdayon 28131 . . . . 5 ( bday ‘𝐵) ∈ On
3 naddcl 8679 . . . . 5 ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
41, 2, 3mp2an 705 . . . 4 (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
5 bdayon 28131 . . . . . . 7 ( bday ‘𝐶) ∈ On
6 bdayon 28131 . . . . . . 7 ( bday ‘𝐸) ∈ On
7 naddcl 8679 . . . . . . 7 ((( bday ‘𝐶) ∈ On ∧ ( bday ‘𝐸) ∈ On) → (( bday ‘𝐶) +no ( bday ‘𝐸)) ∈ On)
85, 6, 7mp2an 705 . . . . . 6 (( bday ‘𝐶) +no ( bday ‘𝐸)) ∈ On
9 bdayon 28131 . . . . . . 7 ( bday ‘𝐷) ∈ On
10 bdayon 28131 . . . . . . 7 ( bday ‘𝐹) ∈ On
11 naddcl 8679 . . . . . . 7 ((( bday ‘𝐷) ∈ On ∧ ( bday ‘𝐹) ∈ On) → (( bday ‘𝐷) +no ( bday ‘𝐹)) ∈ On)
129, 10, 11mp2an 705 . . . . . 6 (( bday ‘𝐷) +no ( bday ‘𝐹)) ∈ On
138, 12onun2i 6485 . . . . 5 ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∈ On
14 naddcl 8679 . . . . . . 7 ((( bday ‘𝐶) ∈ On ∧ ( bday ‘𝐹) ∈ On) → (( bday ‘𝐶) +no ( bday ‘𝐹)) ∈ On)
155, 10, 14mp2an 705 . . . . . 6 (( bday ‘𝐶) +no ( bday ‘𝐹)) ∈ On
16 naddcl 8679 . . . . . . 7 ((( bday ‘𝐷) ∈ On ∧ ( bday ‘𝐸) ∈ On) → (( bday ‘𝐷) +no ( bday ‘𝐸)) ∈ On)
179, 6, 16mp2an 705 . . . . . 6 (( bday ‘𝐷) +no ( bday ‘𝐸)) ∈ On
1815, 17onun2i 6485 . . . . 5 ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ∈ On
1913, 18onun2i 6485 . . . 4 (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) ∈ On
204, 19onun2i 6485 . . 3 ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ∈ On
21 risset 3238 . . 3 (((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ∈ On ↔ ∃𝑥 ∈ On 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
2220, 21mpbi 233 . 2 ∃𝑥 ∈ On 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
23 fveq2 6883 . . . . . . . . . . . 12 (𝑎 = 𝑔 → ( bday ‘𝑎) = ( bday ‘𝑔))
2423oveq1d 7433 . . . . . . . . . . 11 (𝑎 = 𝑔 → (( bday ‘𝑎) +no ( bday ‘𝑏)) = (( bday ‘𝑔) +no ( bday ‘𝑏)))
2524uneq1d 4114 . . . . . . . . . 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 ‘𝑒))))))
2625eqeq2d 2772 . . . . . . . . 9 (𝑎 = 𝑔 → (𝑥 = ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ↔ 𝑥 = ((( bday ‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒)))))))
27 oveq1 7425 . . . . . . . . . . 11 (𝑎 = 𝑔 → (𝑎 ·s 𝑏) = (𝑔 ·s 𝑏))
2827eleq1d 2846 . . . . . . . . . 10 (𝑎 = 𝑔 → ((𝑎 ·s 𝑏) ∈ No ↔ (𝑔 ·s 𝑏) ∈ No ))
2928anbi1d 643 . . . . . . . . 9 (𝑎 = 𝑔 → (((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
3026, 29imbi12d 347 . . . . . . . 8 (𝑎 = 𝑔 → ((𝑥 = ((( 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 ‘𝑒))))) → ((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
31 fveq2 6883 . . . . . . . . . . . 12 (𝑏 = ℎ → ( bday ‘𝑏) = ( bday ‘ℎ))
3231oveq2d 7434 . . . . . . . . . . 11 (𝑏 = ℎ → (( bday ‘𝑔) +no ( bday ‘𝑏)) = (( bday ‘𝑔) +no ( bday ‘ℎ)))
3332uneq1d 4114 . . . . . . . . . 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 ‘𝑒))))))
3433eqeq2d 2772 . . . . . . . . 9 (𝑏 = ℎ → (𝑥 = ((( bday ‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ↔ 𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒)))))))
35 oveq2 7426 . . . . . . . . . . 11 (𝑏 = ℎ → (𝑔 ·s 𝑏) = (𝑔 ·s ℎ))
3635eleq1d 2846 . . . . . . . . . 10 (𝑏 = ℎ → ((𝑔 ·s 𝑏) ∈ No ↔ (𝑔 ·s ℎ) ∈ No ))
3736anbi1d 643 . . . . . . . . 9 (𝑏 = ℎ → (((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
3834, 37imbi12d 347 . . . . . . . 8 (𝑏 = ℎ → ((𝑥 = ((( 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 ‘𝑒))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
39 fveq2 6883 . . . . . . . . . . . . . 14 (𝑐 = 𝑖 → ( bday ‘𝑐) = ( bday ‘𝑖))
4039oveq1d 7433 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (( bday ‘𝑐) +no ( bday ‘𝑒)) = (( bday ‘𝑖) +no ( bday ‘𝑒)))
4140uneq1d 4114 . . . . . . . . . . . 12 (𝑐 = 𝑖 → ((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))))
4239oveq1d 7433 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (( bday ‘𝑐) +no ( bday ‘𝑓)) = (( bday ‘𝑖) +no ( bday ‘𝑓)))
4342uneq1d 4114 . . . . . . . . . . . 12 (𝑐 = 𝑖 → ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))
4441, 43uneq12d 4116 . . . . . . . . . . 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 ‘𝑒)))))
4544uneq2d 4115 . . . . . . . . . 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 ‘𝑒))))))
4645eqeq2d 2772 . . . . . . . . 9 (𝑐 = 𝑖 → (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ↔ 𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒)))))))
47 breq1 5106 . . . . . . . . . . . 12 (𝑐 = 𝑖 → (𝑐 <s 𝑑 ↔ 𝑖 <s 𝑑))
4847anbi1d 643 . . . . . . . . . . 11 (𝑐 = 𝑖 → ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓)))
49 oveq1 7425 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (𝑐 ·s 𝑓) = (𝑖 ·s 𝑓))
50 oveq1 7425 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (𝑐 ·s 𝑒) = (𝑖 ·s 𝑒))
5149, 50oveq12d 7436 . . . . . . . . . . . 12 (𝑐 = 𝑖 → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)))
5251breq1d 5113 . . . . . . . . . . 11 (𝑐 = 𝑖 → (((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))
5348, 52imbi12d 347 . . . . . . . . . 10 (𝑐 = 𝑖 → (((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))
5453anbi2d 642 . . . . . . . . 9 (𝑐 = 𝑖 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
5546, 54imbi12d 347 . . . . . . . 8 (𝑐 = 𝑖 → ((𝑥 = ((( 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 ‘𝑒))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
56 fveq2 6883 . . . . . . . . . . . . . 14 (𝑑 = 𝑗 → ( bday ‘𝑑) = ( bday ‘𝑗))
5756oveq1d 7433 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (( bday ‘𝑑) +no ( bday ‘𝑓)) = (( bday ‘𝑗) +no ( bday ‘𝑓)))
5857uneq2d 4115 . . . . . . . . . . . 12 (𝑑 = 𝑗 → ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))))
5956oveq1d 7433 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (( bday ‘𝑑) +no ( bday ‘𝑒)) = (( bday ‘𝑗) +no ( bday ‘𝑒)))
6059uneq2d 4115 . . . . . . . . . . . 12 (𝑑 = 𝑗 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))
6158, 60uneq12d 4116 . . . . . . . . . . 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 ‘𝑒)))))
6261uneq2d 4115 . . . . . . . . . 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 ‘𝑒))))))
6362eqeq2d 2772 . . . . . . . . 9 (𝑑 = 𝑗 → (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ↔ 𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒)))))))
64 breq2 5107 . . . . . . . . . . . 12 (𝑑 = 𝑗 → (𝑖 <s 𝑑 ↔ 𝑖 <s 𝑗))
6564anbi1d 643 . . . . . . . . . . 11 (𝑑 = 𝑗 → ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓)))
66 oveq1 7425 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (𝑑 ·s 𝑓) = (𝑗 ·s 𝑓))
67 oveq1 7425 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (𝑑 ·s 𝑒) = (𝑗 ·s 𝑒))
6866, 67oveq12d 7436 . . . . . . . . . . . 12 (𝑑 = 𝑗 → ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))
6968breq2d 5115 . . . . . . . . . . 11 (𝑑 = 𝑗 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))
7065, 69imbi12d 347 . . . . . . . . . 10 (𝑑 = 𝑗 → (((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))))
7170anbi2d 642 . . . . . . . . 9 (𝑑 = 𝑗 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))))
7263, 71imbi12d 347 . . . . . . . 8 (𝑑 = 𝑗 → ((𝑥 = ((( 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 ‘𝑒))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))))))
73 fveq2 6883 . . . . . . . . . . . . . 14 (𝑒 = 𝑘 → ( bday ‘𝑒) = ( bday ‘𝑘))
7473oveq2d 7434 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (( bday ‘𝑖) +no ( bday ‘𝑒)) = (( bday ‘𝑖) +no ( bday ‘𝑘)))
7574uneq1d 4114 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))))
7673oveq2d 7434 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (( bday ‘𝑗) +no ( bday ‘𝑒)) = (( bday ‘𝑗) +no ( bday ‘𝑘)))
7776uneq2d 4115 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))
7875, 77uneq12d 4116 . . . . . . . . . . 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 ‘𝑘)))))
7978uneq2d 4115 . . . . . . . . . 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 ‘𝑘))))))
8079eqeq2d 2772 . . . . . . . . 9 (𝑒 = 𝑘 → (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))) ↔ 𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))))
81 breq1 5106 . . . . . . . . . . . 12 (𝑒 = 𝑘 → (𝑒 <s 𝑓 ↔ 𝑘 <s 𝑓))
8281anbi2d 642 . . . . . . . . . . 11 (𝑒 = 𝑘 → ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓)))
83 oveq2 7426 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (𝑖 ·s 𝑒) = (𝑖 ·s 𝑘))
8483oveq2d 7434 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)))
85 oveq2 7426 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (𝑗 ·s 𝑒) = (𝑗 ·s 𝑘))
8685oveq2d 7434 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))
8784, 86breq12d 5116 . . . . . . . . . . 11 (𝑒 = 𝑘 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))
8882, 87imbi12d 347 . . . . . . . . . 10 (𝑒 = 𝑘 → (((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))) ↔ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))))
8988anbi2d 642 . . . . . . . . 9 (𝑒 = 𝑘 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))))
9080, 89imbi12d 347 . . . . . . . 8 (𝑒 = 𝑘 → ((𝑥 = ((( 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 ‘𝑘))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))))))
91 fveq2 6883 . . . . . . . . . . . . . 14 (𝑓 = 𝑙 → ( bday ‘𝑓) = ( bday ‘𝑙))
9291oveq2d 7434 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (( bday ‘𝑗) +no ( bday ‘𝑓)) = (( bday ‘𝑗) +no ( bday ‘𝑙)))
9392uneq2d 4115 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))))
9491oveq2d 7434 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (( bday ‘𝑖) +no ( bday ‘𝑓)) = (( bday ‘𝑖) +no ( bday ‘𝑙)))
9594uneq1d 4114 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))) = ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))
9693, 95uneq12d 4116 . . . . . . . . . . 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 ‘𝑘)))))
9796uneq2d 4115 . . . . . . . . . 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 ‘𝑘))))))
9897eqeq2d 2772 . . . . . . . . 9 (𝑓 = 𝑙 → (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ↔ 𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))))
99 breq2 5107 . . . . . . . . . . . 12 (𝑓 = 𝑙 → (𝑘 <s 𝑓 ↔ 𝑘 <s 𝑙))
10099anbi2d 642 . . . . . . . . . . 11 (𝑓 = 𝑙 → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)))
101 oveq2 7426 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (𝑖 ·s 𝑓) = (𝑖 ·s 𝑙))
102101oveq1d 7433 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) = ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)))
103 oveq2 7426 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (𝑗 ·s 𝑓) = (𝑗 ·s 𝑙))
104103oveq1d 7433 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) = ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))
105102, 104breq12d 5116 . . . . . . . . . . 11 (𝑓 = 𝑙 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) ↔ ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))
106100, 105imbi12d 347 . . . . . . . . . 10 (𝑓 = 𝑙 → (((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))) ↔ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))
107106anbi2d 642 . . . . . . . . 9 (𝑓 = 𝑙 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
10898, 107imbi12d 347 . . . . . . . 8 (𝑓 = 𝑙 → ((𝑥 = ((( 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 ‘𝑘))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
10930, 38, 55, 72, 90, 108cbvral6vw 3249 . . . . . . 7 (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑥 = ((( 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 ‘𝑘))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
110 eqeq1 2765 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥 = ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ↔ 𝑦 = ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒)))))))
111110imbi1d 344 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥 = ((( 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 ‘𝑒))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
1121116ralbidv 3232 . . . . . . 7 (𝑥 = 𝑦 → (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑥 = ((( 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 ‘𝑒))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
113109, 112bitr3id 288 . . . . . 6 (𝑥 = 𝑦 → (∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (𝑥 = ((( 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 ‘𝑒))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
114 raleq 3317 . . . . . . . . . . . . . 14 (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) → (∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ‘𝑘)))))∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 𝑒)))))))
115 ralrot3 3294 . . . . . . . . . . . . . . 15 (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ‘𝑘)))))∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 𝑒))))))
116 ralrot3 3294 . . . . . . . . . . . . . . . . 17 (∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ‘𝑘)))))∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 𝑒))))))
117 ralrot3 3294 . . . . . . . . . . . . . . . . . . 19 (∀𝑒 ∈ 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 𝑒))))) ↔ ∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 𝑒))))))
118 r19.23v 3190 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( 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 𝑒))))))
119 risset 3238 . . . . . . . . . . . . . . . . . . . . . 22 (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ↔ ∃𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))𝑦 = ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))))
120119imbi1i 352 . . . . . . . . . . . . . . . . . . . . 21 ((((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( 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 𝑒))))))
121118, 120bitr4i 281 . . . . . . . . . . . . . . . . . . . 20 (∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( 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 𝑒))))))
1221212ralbii 3138 . . . . . . . . . . . . . . . . . . 19 (∀𝑒 ∈ 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 (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( 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 𝑒))))))
123117, 122bitr3i 280 . . . . . . . . . . . . . . . . . 18 (∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( 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 𝑒))))))
1241232ralbii 3138 . . . . . . . . . . . . . . . . 17 (∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( 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 𝑒))))))
125116, 124bitr3i 280 . . . . . . . . . . . . . . . 16 (∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( 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 𝑒))))))
1261252ralbii 3138 . . . . . . . . . . . . . . 15 (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 𝑒))))))
127115, 126bitr3i 280 . . . . . . . . . . . . . 14 (∀𝑦 ∈ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 𝑒))))))
128114, 127bitrdi 290 . . . . . . . . . . . . 13 (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) → (∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 𝑒)))))))
129 simpl 488 . . . . . . . . . . . . . . . 16 ((∀𝑎 ∈ 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 ))) → ∀𝑎 ∈ 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 𝑒))))))
130 simprl1 1237 . . . . . . . . . . . . . . . 16 ((∀𝑎 ∈ 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 ))) → 𝑔 ∈ No )
131 simprl2 1238 . . . . . . . . . . . . . . . 16 ((∀𝑎 ∈ 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 ))) → ℎ ∈ No )
132129, 130, 131mulsproplem11 28505 . . . . . . . . . . . . . . 15 ((∀𝑎 ∈ 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 ))) → (𝑔 ·s ℎ) ∈ No )
133129adantr 486 . . . . . . . . . . . . . . . . 17 (((∀𝑎 ∈ 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 ))) ∧ (𝑖 <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 𝑒))))))
134 simprl3 1239 . . . . . . . . . . . . . . . . . 18 ((∀𝑎 ∈ 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 ))) → 𝑖 ∈ No )
135134adantr 486 . . . . . . . . . . . . . . . . 17 (((∀𝑎 ∈ 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 ))) ∧ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)) → 𝑖 ∈ No )
136 simprr1 1240 . . . . . . . . . . . . . . . . . 18 ((∀𝑎 ∈ 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 ))) → 𝑗 ∈ No )
137136adantr 486 . . . . . . . . . . . . . . . . 17 (((∀𝑎 ∈ 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 ))) ∧ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)) → 𝑗 ∈ No )
138 simprr2 1241 . . . . . . . . . . . . . . . . . 18 ((∀𝑎 ∈ 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 ))) → 𝑘 ∈ No )
139138adantr 486 . . . . . . . . . . . . . . . . 17 (((∀𝑎 ∈ 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 ))) ∧ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)) → 𝑘 ∈ No )
140 simprr3 1242 . . . . . . . . . . . . . . . . . 18 ((∀𝑎 ∈ 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 ))) → 𝑙 ∈ No )
141140adantr 486 . . . . . . . . . . . . . . . . 17 (((∀𝑎 ∈ 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 ))) ∧ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)) → 𝑙 ∈ No )
142 simprl 783 . . . . . . . . . . . . . . . . 17 (((∀𝑎 ∈ 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 ))) ∧ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)) → 𝑖 <s 𝑗)
143 simprr 785 . . . . . . . . . . . . . . . . 17 (((∀𝑎 ∈ 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 ))) ∧ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)) → 𝑘 <s 𝑙)
144133, 135, 137, 139, 141, 142, 143mulsproplem14 28508 . . . . . . . . . . . . . . . 16 (((∀𝑎 ∈ 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 ))) ∧ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))
145144ex 418 . . . . . . . . . . . . . . 15 ((∀𝑎 ∈ 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 ))) → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))
146132, 145jca 521 . . . . . . . . . . . . . 14 ((∀𝑎 ∈ 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 ))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))
147146ex 418 . . . . . . . . . . . . 13 (∀𝑎 ∈ 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 )) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
148128, 147biimtrdi 256 . . . . . . . . . . . 12 (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) → (∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 )) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
149148impd 416 . . . . . . . . . . 11 (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) → ((∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
150149com12 33 . . . . . . . . . 10 ((∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ‘𝑘))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
151150anassrs 473 . . . . . . . . 9 (((∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ‘𝑘))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
152151ralrimivvva 3209 . . . . . . . 8 ((∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ‘𝑘))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
153152ralrimivvva 3209 . . . . . . 7 (∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ‘𝑘))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
154153a1i 11 . . . . . 6 (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (𝑦 = ((( 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 ‘𝑘))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
155113, 154tfis2 7866 . . . . 5 (𝑥 ∈ On → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (𝑥 = ((( 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 𝑘))))))
156 fveq2 6883 . . . . . . . . . 10 (𝑔 = 𝐴 → ( bday ‘𝑔) = ( bday ‘𝐴))
157156oveq1d 7433 . . . . . . . . 9 (𝑔 = 𝐴 → (( bday ‘𝑔) +no ( bday ‘ℎ)) = (( bday ‘𝐴) +no ( bday ‘ℎ)))
158157uneq1d 4114 . . . . . . . 8 (𝑔 = 𝐴 → ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) = ((( bday ‘𝐴) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))))
159158eqeq2d 2772 . . . . . . 7 (𝑔 = 𝐴 → (𝑥 = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ↔ 𝑥 = ((( bday ‘𝐴) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))))
160 oveq1 7425 . . . . . . . . 9 (𝑔 = 𝐴 → (𝑔 ·s ℎ) = (𝐴 ·s ℎ))
161160eleq1d 2846 . . . . . . . 8 (𝑔 = 𝐴 → ((𝑔 ·s ℎ) ∈ No ↔ (𝐴 ·s ℎ) ∈ No ))
162161anbi1d 643 . . . . . . 7 (𝑔 = 𝐴 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))) ↔ ((𝐴 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
163159, 162imbi12d 347 . . . . . 6 (𝑔 = 𝐴 → ((𝑥 = ((( 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 ‘𝑘))))) → ((𝐴 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
164 fveq2 6883 . . . . . . . . . 10 (ℎ = 𝐵 → ( bday ‘ℎ) = ( bday ‘𝐵))
165164oveq2d 7434 . . . . . . . . 9 (ℎ = 𝐵 → (( bday ‘𝐴) +no ( bday ‘ℎ)) = (( bday ‘𝐴) +no ( bday ‘𝐵)))
166165uneq1d 4114 . . . . . . . 8 (ℎ = 𝐵 → ((( bday ‘𝐴) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))))
167166eqeq2d 2772 . . . . . . 7 (ℎ = 𝐵 → (𝑥 = ((( bday ‘𝐴) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ↔ 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))))
168 oveq2 7426 . . . . . . . . 9 (ℎ = 𝐵 → (𝐴 ·s ℎ) = (𝐴 ·s 𝐵))
169168eleq1d 2846 . . . . . . . 8 (ℎ = 𝐵 → ((𝐴 ·s ℎ) ∈ No ↔ (𝐴 ·s 𝐵) ∈ No ))
170169anbi1d 643 . . . . . . 7 (ℎ = 𝐵 → (((𝐴 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))) ↔ ((𝐴 ·s 𝐵) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
171167, 170imbi12d 347 . . . . . 6 (ℎ = 𝐵 → ((𝑥 = ((( 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 ‘𝑘))))) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
172 fveq2 6883 . . . . . . . . . . . 12 (𝑖 = 𝐶 → ( bday ‘𝑖) = ( bday ‘𝐶))
173172oveq1d 7433 . . . . . . . . . . 11 (𝑖 = 𝐶 → (( bday ‘𝑖) +no ( bday ‘𝑘)) = (( bday ‘𝐶) +no ( bday ‘𝑘)))
174173uneq1d 4114 . . . . . . . . . 10 (𝑖 = 𝐶 → ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) = ((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))))
175172oveq1d 7433 . . . . . . . . . . 11 (𝑖 = 𝐶 → (( bday ‘𝑖) +no ( bday ‘𝑙)) = (( bday ‘𝐶) +no ( bday ‘𝑙)))
176175uneq1d 4114 . . . . . . . . . 10 (𝑖 = 𝐶 → ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))) = ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))
177174, 176uneq12d 4116 . . . . . . . . 9 (𝑖 = 𝐶 → (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))) = (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))
178177uneq2d 4115 . . . . . . . 8 (𝑖 = 𝐶 → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))))
179178eqeq2d 2772 . . . . . . 7 (𝑖 = 𝐶 → (𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ↔ 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))))
180 breq1 5106 . . . . . . . . . 10 (𝑖 = 𝐶 → (𝑖 <s 𝑗 ↔ 𝐶 <s 𝑗))
181180anbi1d 643 . . . . . . . . 9 (𝑖 = 𝐶 → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙)))
182 oveq1 7425 . . . . . . . . . . 11 (𝑖 = 𝐶 → (𝑖 ·s 𝑙) = (𝐶 ·s 𝑙))
183 oveq1 7425 . . . . . . . . . . 11 (𝑖 = 𝐶 → (𝑖 ·s 𝑘) = (𝐶 ·s 𝑘))
184182, 183oveq12d 7436 . . . . . . . . . 10 (𝑖 = 𝐶 → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) = ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)))
185184breq1d 5113 . . . . . . . . 9 (𝑖 = 𝐶 → (((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)) ↔ ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))
186181, 185imbi12d 347 . . . . . . . 8 (𝑖 = 𝐶 → (((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))) ↔ ((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))
187186anbi2d 642 . . . . . . 7 (𝑖 = 𝐶 → (((𝐴 ·s 𝐵) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))) ↔ ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
188179, 187imbi12d 347 . . . . . 6 (𝑖 = 𝐶 → ((𝑥 = ((( 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 ‘𝑘))))) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
189 fveq2 6883 . . . . . . . . . . . 12 (𝑗 = 𝐷 → ( bday ‘𝑗) = ( bday ‘𝐷))
190189oveq1d 7433 . . . . . . . . . . 11 (𝑗 = 𝐷 → (( bday ‘𝑗) +no ( bday ‘𝑙)) = (( bday ‘𝐷) +no ( bday ‘𝑙)))
191190uneq2d 4115 . . . . . . . . . 10 (𝑗 = 𝐷 → ((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) = ((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))))
192189oveq1d 7433 . . . . . . . . . . 11 (𝑗 = 𝐷 → (( bday ‘𝑗) +no ( bday ‘𝑘)) = (( bday ‘𝐷) +no ( bday ‘𝑘)))
193192uneq2d 4115 . . . . . . . . . 10 (𝑗 = 𝐷 → ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))) = ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘))))
194191, 193uneq12d 4116 . . . . . . . . 9 (𝑗 = 𝐷 → (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))) = (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘)))))
195194uneq2d 4115 . . . . . . . 8 (𝑗 = 𝐷 → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘))))))
196195eqeq2d 2772 . . . . . . 7 (𝑗 = 𝐷 → (𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ↔ 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘)))))))
197 breq2 5107 . . . . . . . . . 10 (𝑗 = 𝐷 → (𝐶 <s 𝑗 ↔ 𝐶 <s 𝐷))
198197anbi1d 643 . . . . . . . . 9 (𝑗 = 𝐷 → ((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙)))
199 oveq1 7425 . . . . . . . . . . 11 (𝑗 = 𝐷 → (𝑗 ·s 𝑙) = (𝐷 ·s 𝑙))
200 oveq1 7425 . . . . . . . . . . 11 (𝑗 = 𝐷 → (𝑗 ·s 𝑘) = (𝐷 ·s 𝑘))
201199, 200oveq12d 7436 . . . . . . . . . 10 (𝑗 = 𝐷 → ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)) = ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)))
202201breq2d 5115 . . . . . . . . 9 (𝑗 = 𝐷 → (((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)) ↔ ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘))))
203198, 202imbi12d 347 . . . . . . . 8 (𝑗 = 𝐷 → (((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))) ↔ ((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)))))
204203anbi2d 642 . . . . . . 7 (𝑗 = 𝐷 → (((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))) ↔ ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘))))))
205196, 204imbi12d 347 . . . . . 6 (𝑗 = 𝐷 → ((𝑥 = ((( 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 ‘𝑘))))) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)))))))
206 fveq2 6883 . . . . . . . . . . . 12 (𝑘 = 𝐸 → ( bday ‘𝑘) = ( bday ‘𝐸))
207206oveq2d 7434 . . . . . . . . . . 11 (𝑘 = 𝐸 → (( bday ‘𝐶) +no ( bday ‘𝑘)) = (( bday ‘𝐶) +no ( bday ‘𝐸)))
208207uneq1d 4114 . . . . . . . . . 10 (𝑘 = 𝐸 → ((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) = ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))))
209206oveq2d 7434 . . . . . . . . . . 11 (𝑘 = 𝐸 → (( bday ‘𝐷) +no ( bday ‘𝑘)) = (( bday ‘𝐷) +no ( bday ‘𝐸)))
210209uneq2d 4115 . . . . . . . . . 10 (𝑘 = 𝐸 → ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘))) = ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
211208, 210uneq12d 4116 . . . . . . . . 9 (𝑘 = 𝐸 → (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘)))) = (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
212211uneq2d 4115 . . . . . . . 8 (𝑘 = 𝐸 → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘))))) = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
213212eqeq2d 2772 . . . . . . 7 (𝑘 = 𝐸 → (𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘))))) ↔ 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
214 breq1 5106 . . . . . . . . . 10 (𝑘 = 𝐸 → (𝑘 <s 𝑙 ↔ 𝐸 <s 𝑙))
215214anbi2d 642 . . . . . . . . 9 (𝑘 = 𝐸 → ((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙)))
216 oveq2 7426 . . . . . . . . . . 11 (𝑘 = 𝐸 → (𝐶 ·s 𝑘) = (𝐶 ·s 𝐸))
217216oveq2d 7434 . . . . . . . . . 10 (𝑘 = 𝐸 → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) = ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)))
218 oveq2 7426 . . . . . . . . . . 11 (𝑘 = 𝐸 → (𝐷 ·s 𝑘) = (𝐷 ·s 𝐸))
219218oveq2d 7434 . . . . . . . . . 10 (𝑘 = 𝐸 → ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)) = ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)))
220217, 219breq12d 5116 . . . . . . . . 9 (𝑘 = 𝐸 → (((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)) ↔ ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸))))
221215, 220imbi12d 347 . . . . . . . 8 (𝑘 = 𝐸 → (((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘))) ↔ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)))))
222221anbi2d 642 . . . . . . 7 (𝑘 = 𝐸 → (((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)))) ↔ ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸))))))
223213, 222imbi12d 347 . . . . . 6 (𝑘 = 𝐸 → ((𝑥 = ((( 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 ‘𝐸))))) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)))))))
224 fveq2 6883 . . . . . . . . . . . 12 (𝑙 = 𝐹 → ( bday ‘𝑙) = ( bday ‘𝐹))
225224oveq2d 7434 . . . . . . . . . . 11 (𝑙 = 𝐹 → (( bday ‘𝐷) +no ( bday ‘𝑙)) = (( bday ‘𝐷) +no ( bday ‘𝐹)))
226225uneq2d 4115 . . . . . . . . . 10 (𝑙 = 𝐹 → ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) = ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))))
227224oveq2d 7434 . . . . . . . . . . 11 (𝑙 = 𝐹 → (( bday ‘𝐶) +no ( bday ‘𝑙)) = (( bday ‘𝐶) +no ( bday ‘𝐹)))
228227uneq1d 4114 . . . . . . . . . 10 (𝑙 = 𝐹 → ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) = ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
229226, 228uneq12d 4116 . . . . . . . . 9 (𝑙 = 𝐹 → (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) = (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
230229uneq2d 4115 . . . . . . . 8 (𝑙 = 𝐹 → ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))))
231230eqeq2d 2772 . . . . . . 7 (𝑙 = 𝐹 → (𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ↔ 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
232 breq2 5107 . . . . . . . . . 10 (𝑙 = 𝐹 → (𝐸 <s 𝑙 ↔ 𝐸 <s 𝐹))
233232anbi2d 642 . . . . . . . . 9 (𝑙 = 𝐹 → ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹)))
234 oveq2 7426 . . . . . . . . . . 11 (𝑙 = 𝐹 → (𝐶 ·s 𝑙) = (𝐶 ·s 𝐹))
235234oveq1d 7433 . . . . . . . . . 10 (𝑙 = 𝐹 → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)))
236 oveq2 7426 . . . . . . . . . . 11 (𝑙 = 𝐹 → (𝐷 ·s 𝑙) = (𝐷 ·s 𝐹))
237236oveq1d 7433 . . . . . . . . . 10 (𝑙 = 𝐹 → ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
238235, 237breq12d 5116 . . . . . . . . 9 (𝑙 = 𝐹 → (((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
239233, 238imbi12d 347 . . . . . . . 8 (𝑙 = 𝐹 → (((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸))) ↔ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
240239anbi2d 642 . . . . . . 7 (𝑙 = 𝐹 → (((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)))) ↔ ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))))
241231, 240imbi12d 347 . . . . . 6 (𝑙 = 𝐹 → ((𝑥 = ((( 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 ‘𝐸))))) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))))
242163, 171, 188, 205, 223, 241rspc6v 3597 . . . . 5 (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ (𝐸 ∈ No ∧ 𝐹 ∈ No )) → (∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (𝑥 = ((( 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 ‘𝐸))))) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))))
243155, 242syl5com 32 . . . 4 (𝑥 ∈ On → (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ (𝐸 ∈ No ∧ 𝐹 ∈ No )) → (𝑥 = ((( 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 𝐸)))))))
244243com23 87 . . 3 (𝑥 ∈ On → (𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ (𝐸 ∈ No ∧ 𝐹 ∈ No )) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))))
245244rexlimiv 3157 . 2 (∃𝑥 ∈ On 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ (𝐸 ∈ No ∧ 𝐹 ∈ No )) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))))
24622, 245ax-mp 5 1 (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ (𝐸 ∈ No ∧ 𝐹 ∈ No )) → ((𝐴 ·s 𝐵) ∈ No ∧ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087   ∪ cun 3897   class class class wbr 5103  Oncon0 6361  ‘cfv 6537  (class class class)co 7418   +no cnadd 8667   No csur 27990   <s clts 27991   bday cbday 27992   -s csubs 28399   ·s cmuls 28485
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-1o 8469  df-2o 8470  df-nadd 8668  df-no 27993  df-lts 27994  df-bday 27995  df-les 28095  df-slts 28137  df-cuts 28139  df-0s 28186  df-made 28206  df-old 28207  df-left 28209  df-right 28210  df-norec 28317  df-norec2 28328  df-adds 28339  df-negs 28400  df-subs 28401  df-muls 28486
This theorem is used by:  mulcutlem  28510  mulscl  28513  ltmuls  28515
  Copyright terms: Public domain W3C validator