MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsprop Structured version   Visualization version   GIF version
Theorem mulsprop 27515
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 bdayelon 27207 . . . . 5 ( bday ‘𝐴) ∈ On
2 bdayelon 27207 . . . . 5 ( bday ‘𝐵) ∈ On
3 naddcl 8661 . . . . 5 ((( bday ‘𝐴) ∈ On ∧ ( bday ‘𝐵) ∈ On) → (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On)
41, 2, 3mp2an 690 . . . 4 (( bday ‘𝐴) +no ( bday ‘𝐵)) ∈ On
5 bdayelon 27207 . . . . . . 7 ( bday ‘𝐶) ∈ On
6 bdayelon 27207 . . . . . . 7 ( bday ‘𝐸) ∈ On
7 naddcl 8661 . . . . . . 7 ((( bday ‘𝐶) ∈ On ∧ ( bday ‘𝐸) ∈ On) → (( bday ‘𝐶) +no ( bday ‘𝐸)) ∈ On)
85, 6, 7mp2an 690 . . . . . 6 (( bday ‘𝐶) +no ( bday ‘𝐸)) ∈ On
9 bdayelon 27207 . . . . . . 7 ( bday ‘𝐷) ∈ On
10 bdayelon 27207 . . . . . . 7 ( bday ‘𝐹) ∈ On
11 naddcl 8661 . . . . . . 7 ((( bday ‘𝐷) ∈ On ∧ ( bday ‘𝐹) ∈ On) → (( bday ‘𝐷) +no ( bday ‘𝐹)) ∈ On)
129, 10, 11mp2an 690 . . . . . 6 (( bday ‘𝐷) +no ( bday ‘𝐹)) ∈ On
138, 12onun2i 6476 . . . . 5 ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∈ On
14 naddcl 8661 . . . . . . 7 ((( bday ‘𝐶) ∈ On ∧ ( bday ‘𝐹) ∈ On) → (( bday ‘𝐶) +no ( bday ‘𝐹)) ∈ On)
155, 10, 14mp2an 690 . . . . . 6 (( bday ‘𝐶) +no ( bday ‘𝐹)) ∈ On
16 naddcl 8661 . . . . . . 7 ((( bday ‘𝐷) ∈ On ∧ ( bday ‘𝐸) ∈ On) → (( bday ‘𝐷) +no ( bday ‘𝐸)) ∈ On)
179, 6, 16mp2an 690 . . . . . 6 (( bday ‘𝐷) +no ( bday ‘𝐸)) ∈ On
1815, 17onun2i 6476 . . . . 5 ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) ∈ On
1913, 18onun2i 6476 . . . 4 (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))) ∈ On
204, 19onun2i 6476 . . 3 ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ∈ On
21 risset 3230 . . 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 229 . 2 ∃𝑥 ∈ On 𝑥 = ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))
23 fveq2 6879 . . . . . . . . . . . 12 (𝑎 = 𝑔 → ( bday ‘𝑎) = ( bday ‘𝑔))
2423oveq1d 7409 . . . . . . . . . . 11 (𝑎 = 𝑔 → (( bday ‘𝑎) +no ( bday ‘𝑏)) = (( bday ‘𝑔) +no ( bday ‘𝑏)))
2524uneq1d 4159 . . . . . . . . . 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 2743 . . . . . . . . 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 7401 . . . . . . . . . . 11 (𝑎 = 𝑔 → (𝑎 ·s 𝑏) = (𝑔 ·s 𝑏))
2827eleq1d 2818 . . . . . . . . . 10 (𝑎 = 𝑔 → ((𝑎 ·s 𝑏) ∈ No ↔ (𝑔 ·s 𝑏) ∈ No ))
2928anbi1d 630 . . . . . . . . 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 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 𝑒)))))))
31 fveq2 6879 . . . . . . . . . . . 12 (𝑏 = ℎ → ( bday ‘𝑏) = ( bday ‘ℎ))
3231oveq2d 7410 . . . . . . . . . . 11 (𝑏 = ℎ → (( bday ‘𝑔) +no ( bday ‘𝑏)) = (( bday ‘𝑔) +no ( bday ‘ℎ)))
3332uneq1d 4159 . . . . . . . . . 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 2743 . . . . . . . . 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 7402 . . . . . . . . . . 11 (𝑏 = ℎ → (𝑔 ·s 𝑏) = (𝑔 ·s ℎ))
3635eleq1d 2818 . . . . . . . . . 10 (𝑏 = ℎ → ((𝑔 ·s 𝑏) ∈ No ↔ (𝑔 ·s ℎ) ∈ No ))
3736anbi1d 630 . . . . . . . . 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 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 𝑒)))))))
39 fveq2 6879 . . . . . . . . . . . . . 14 (𝑐 = 𝑖 → ( bday ‘𝑐) = ( bday ‘𝑖))
4039oveq1d 7409 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (( bday ‘𝑐) +no ( bday ‘𝑒)) = (( bday ‘𝑖) +no ( bday ‘𝑒)))
4140uneq1d 4159 . . . . . . . . . . . 12 (𝑐 = 𝑖 → ((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))))
4239oveq1d 7409 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (( bday ‘𝑐) +no ( bday ‘𝑓)) = (( bday ‘𝑖) +no ( bday ‘𝑓)))
4342uneq1d 4159 . . . . . . . . . . . 12 (𝑐 = 𝑖 → ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))
4441, 43uneq12d 4161 . . . . . . . . . . 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 4160 . . . . . . . . . 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 2743 . . . . . . . . 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 5145 . . . . . . . . . . . 12 (𝑐 = 𝑖 → (𝑐 <s 𝑑 ↔ 𝑖 <s 𝑑))
4847anbi1d 630 . . . . . . . . . . 11 (𝑐 = 𝑖 → ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓)))
49 oveq1 7401 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (𝑐 ·s 𝑓) = (𝑖 ·s 𝑓))
50 oveq1 7401 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (𝑐 ·s 𝑒) = (𝑖 ·s 𝑒))
5149, 50oveq12d 7412 . . . . . . . . . . . 12 (𝑐 = 𝑖 → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)))
5251breq1d 5152 . . . . . . . . . . 11 (𝑐 = 𝑖 → (((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))
5348, 52imbi12d 344 . . . . . . . . . 10 (𝑐 = 𝑖 → (((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))
5453anbi2d 629 . . . . . . . . 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 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 𝑒)))))))
56 fveq2 6879 . . . . . . . . . . . . . 14 (𝑑 = 𝑗 → ( bday ‘𝑑) = ( bday ‘𝑗))
5756oveq1d 7409 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (( bday ‘𝑑) +no ( bday ‘𝑓)) = (( bday ‘𝑗) +no ( bday ‘𝑓)))
5857uneq2d 4160 . . . . . . . . . . . 12 (𝑑 = 𝑗 → ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))))
5956oveq1d 7409 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (( bday ‘𝑑) +no ( bday ‘𝑒)) = (( bday ‘𝑗) +no ( bday ‘𝑒)))
6059uneq2d 4160 . . . . . . . . . . . 12 (𝑑 = 𝑗 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))
6158, 60uneq12d 4161 . . . . . . . . . . 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 4160 . . . . . . . . . 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 2743 . . . . . . . . 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 5146 . . . . . . . . . . . 12 (𝑑 = 𝑗 → (𝑖 <s 𝑑 ↔ 𝑖 <s 𝑗))
6564anbi1d 630 . . . . . . . . . . 11 (𝑑 = 𝑗 → ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓)))
66 oveq1 7401 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (𝑑 ·s 𝑓) = (𝑗 ·s 𝑓))
67 oveq1 7401 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (𝑑 ·s 𝑒) = (𝑗 ·s 𝑒))
6866, 67oveq12d 7412 . . . . . . . . . . . 12 (𝑑 = 𝑗 → ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))
6968breq2d 5154 . . . . . . . . . . 11 (𝑑 = 𝑗 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))
7065, 69imbi12d 344 . . . . . . . . . 10 (𝑑 = 𝑗 → (((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))))
7170anbi2d 629 . . . . . . . . 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 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 𝑒)))))))
73 fveq2 6879 . . . . . . . . . . . . . 14 (𝑒 = 𝑘 → ( bday ‘𝑒) = ( bday ‘𝑘))
7473oveq2d 7410 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (( bday ‘𝑖) +no ( bday ‘𝑒)) = (( bday ‘𝑖) +no ( bday ‘𝑘)))
7574uneq1d 4159 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))))
7673oveq2d 7410 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (( bday ‘𝑗) +no ( bday ‘𝑒)) = (( bday ‘𝑗) +no ( bday ‘𝑘)))
7776uneq2d 4160 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))
7875, 77uneq12d 4161 . . . . . . . . . . 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 4160 . . . . . . . . . 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 2743 . . . . . . . . 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 5145 . . . . . . . . . . . 12 (𝑒 = 𝑘 → (𝑒 <s 𝑓 ↔ 𝑘 <s 𝑓))
8281anbi2d 629 . . . . . . . . . . 11 (𝑒 = 𝑘 → ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓)))
83 oveq2 7402 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (𝑖 ·s 𝑒) = (𝑖 ·s 𝑘))
8483oveq2d 7410 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)))
85 oveq2 7402 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (𝑗 ·s 𝑒) = (𝑗 ·s 𝑘))
8685oveq2d 7410 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))
8784, 86breq12d 5155 . . . . . . . . . . 11 (𝑒 = 𝑘 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))
8882, 87imbi12d 344 . . . . . . . . . 10 (𝑒 = 𝑘 → (((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))) ↔ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))))
8988anbi2d 629 . . . . . . . . 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 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 𝑘)))))))
91 fveq2 6879 . . . . . . . . . . . . . 14 (𝑓 = 𝑙 → ( bday ‘𝑓) = ( bday ‘𝑙))
9291oveq2d 7410 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (( bday ‘𝑗) +no ( bday ‘𝑓)) = (( bday ‘𝑗) +no ( bday ‘𝑙)))
9392uneq2d 4160 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))))
9491oveq2d 7410 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (( bday ‘𝑖) +no ( bday ‘𝑓)) = (( bday ‘𝑖) +no ( bday ‘𝑙)))
9594uneq1d 4159 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))) = ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))
9693, 95uneq12d 4161 . . . . . . . . . . 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 4160 . . . . . . . . . 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 2743 . . . . . . . . 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 5146 . . . . . . . . . . . 12 (𝑓 = 𝑙 → (𝑘 <s 𝑓 ↔ 𝑘 <s 𝑙))
10099anbi2d 629 . . . . . . . . . . 11 (𝑓 = 𝑙 → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)))
101 oveq2 7402 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (𝑖 ·s 𝑓) = (𝑖 ·s 𝑙))
102101oveq1d 7409 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) = ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)))
103 oveq2 7402 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (𝑗 ·s 𝑓) = (𝑗 ·s 𝑙))
104103oveq1d 7409 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) = ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))
105102, 104breq12d 5155 . . . . . . . . . . 11 (𝑓 = 𝑙 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) ↔ ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))
106100, 105imbi12d 344 . . . . . . . . . 10 (𝑓 = 𝑙 → (((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))) ↔ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))
107106anbi2d 629 . . . . . . . . 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 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 𝑘)))))))
10930, 38, 55, 72, 90, 108cbvral6vw 3242 . . . . . . 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 2736 . . . . . . . . 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 341 . . . . . . . 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 3223 . . . . . . 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 284 . . . . . 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 3322 . . . . . . . . . . . . . 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 3290 . . . . . . . . . . . . . . 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 3290 . . . . . . . . . . . . . . . . 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 3290 . . . . . . . . . . . . . . . . . . 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 3182 . . . . . . . . . . . . . . . . . . . . 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 3230 . . . . . . . . . . . . . . . . . . . . . 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 349 . . . . . . . . . . . . . . . . . . . . 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 277 . . . . . . . . . . . . . . . . . . . 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 3128 . . . . . . . . . . . . . . . . . . 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 276 . . . . . . . . . . . . . . . . . 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 3128 . . . . . . . . . . . . . . . . 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 276 . . . . . . . . . . . . . . . 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 3128 . . . . . . . . . . . . . . 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 276 . . . . . . . . . . . . . 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 286 . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . 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 1219 . . . . . . . . . . . . . . . 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 27511 . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . 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 1220 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . 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 1221 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . 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 1222 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . 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 1223 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . 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 27514 . . . . . . . . . . . . . . . 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 413 . . . . . . . . . . . . . . 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 512 . . . . . . . . . . . . . 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 413 . . . . . . . . . . . . 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, 147syl6bi 252 . . . . . . . . . . . 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 411 . . . . . . . . . . 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 32 . . . . . . . . . 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 468 . . . . . . . . 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 3203 . . . . . . . 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 3203 . . . . . . 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 7830 . . . . 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 6879 . . . . . . . . . 10 (𝑔 = 𝐴 → ( bday ‘𝑔) = ( bday ‘𝐴))
157156oveq1d 7409 . . . . . . . . 9 (𝑔 = 𝐴 → (( bday ‘𝑔) +no ( bday ‘ℎ)) = (( bday ‘𝐴) +no ( bday ‘ℎ)))
158157uneq1d 4159 . . . . . . . 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 2743 . . . . . . 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 7401 . . . . . . . . 9 (𝑔 = 𝐴 → (𝑔 ·s ℎ) = (𝐴 ·s ℎ))
161160eleq1d 2818 . . . . . . . 8 (𝑔 = 𝐴 → ((𝑔 ·s ℎ) ∈ No ↔ (𝐴 ·s ℎ) ∈ No ))
162161anbi1d 630 . . . . . . 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 344 . . . . . 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 6879 . . . . . . . . . 10 (ℎ = 𝐵 → ( bday ‘ℎ) = ( bday ‘𝐵))
165164oveq2d 7410 . . . . . . . . 9 (ℎ = 𝐵 → (( bday ‘𝐴) +no ( bday ‘ℎ)) = (( bday ‘𝐴) +no ( bday ‘𝐵)))
166165uneq1d 4159 . . . . . . . 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 2743 . . . . . . 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 7402 . . . . . . . . 9 (ℎ = 𝐵 → (𝐴 ·s ℎ) = (𝐴 ·s 𝐵))
169168eleq1d 2818 . . . . . . . 8 (ℎ = 𝐵 → ((𝐴 ·s ℎ) ∈ No ↔ (𝐴 ·s 𝐵) ∈ No ))
170169anbi1d 630 . . . . . . 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 344 . . . . . 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 6879 . . . . . . . . . . . 12 (𝑖 = 𝐶 → ( bday ‘𝑖) = ( bday ‘𝐶))
173172oveq1d 7409 . . . . . . . . . . 11 (𝑖 = 𝐶 → (( bday ‘𝑖) +no ( bday ‘𝑘)) = (( bday ‘𝐶) +no ( bday ‘𝑘)))
174173uneq1d 4159 . . . . . . . . . 10 (𝑖 = 𝐶 → ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) = ((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))))
175172oveq1d 7409 . . . . . . . . . . 11 (𝑖 = 𝐶 → (( bday ‘𝑖) +no ( bday ‘𝑙)) = (( bday ‘𝐶) +no ( bday ‘𝑙)))
176175uneq1d 4159 . . . . . . . . . 10 (𝑖 = 𝐶 → ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))) = ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))
177174, 176uneq12d 4161 . . . . . . . . 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 4160 . . . . . . . 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 2743 . . . . . . 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 5145 . . . . . . . . . 10 (𝑖 = 𝐶 → (𝑖 <s 𝑗 ↔ 𝐶 <s 𝑗))
181180anbi1d 630 . . . . . . . . 9 (𝑖 = 𝐶 → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙)))
182 oveq1 7401 . . . . . . . . . . 11 (𝑖 = 𝐶 → (𝑖 ·s 𝑙) = (𝐶 ·s 𝑙))
183 oveq1 7401 . . . . . . . . . . 11 (𝑖 = 𝐶 → (𝑖 ·s 𝑘) = (𝐶 ·s 𝑘))
184182, 183oveq12d 7412 . . . . . . . . . 10 (𝑖 = 𝐶 → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) = ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)))
185184breq1d 5152 . . . . . . . . 9 (𝑖 = 𝐶 → (((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)) ↔ ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))
186181, 185imbi12d 344 . . . . . . . 8 (𝑖 = 𝐶 → (((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))) ↔ ((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))
187186anbi2d 629 . . . . . . 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 344 . . . . . 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 6879 . . . . . . . . . . . 12 (𝑗 = 𝐷 → ( bday ‘𝑗) = ( bday ‘𝐷))
190189oveq1d 7409 . . . . . . . . . . 11 (𝑗 = 𝐷 → (( bday ‘𝑗) +no ( bday ‘𝑙)) = (( bday ‘𝐷) +no ( bday ‘𝑙)))
191190uneq2d 4160 . . . . . . . . . 10 (𝑗 = 𝐷 → ((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) = ((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))))
192189oveq1d 7409 . . . . . . . . . . 11 (𝑗 = 𝐷 → (( bday ‘𝑗) +no ( bday ‘𝑘)) = (( bday ‘𝐷) +no ( bday ‘𝑘)))
193192uneq2d 4160 . . . . . . . . . 10 (𝑗 = 𝐷 → ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))) = ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘))))
194191, 193uneq12d 4161 . . . . . . . . 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 4160 . . . . . . . 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 2743 . . . . . . 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 5146 . . . . . . . . . 10 (𝑗 = 𝐷 → (𝐶 <s 𝑗 ↔ 𝐶 <s 𝐷))
198197anbi1d 630 . . . . . . . . 9 (𝑗 = 𝐷 → ((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙)))
199 oveq1 7401 . . . . . . . . . . 11 (𝑗 = 𝐷 → (𝑗 ·s 𝑙) = (𝐷 ·s 𝑙))
200 oveq1 7401 . . . . . . . . . . 11 (𝑗 = 𝐷 → (𝑗 ·s 𝑘) = (𝐷 ·s 𝑘))
201199, 200oveq12d 7412 . . . . . . . . . 10 (𝑗 = 𝐷 → ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)) = ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)))
202201breq2d 5154 . . . . . . . . 9 (𝑗 = 𝐷 → (((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)) ↔ ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘))))
203198, 202imbi12d 344 . . . . . . . 8 (𝑗 = 𝐷 → (((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))) ↔ ((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)))))
204203anbi2d 629 . . . . . . 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 344 . . . . . 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 6879 . . . . . . . . . . . 12 (𝑘 = 𝐸 → ( bday ‘𝑘) = ( bday ‘𝐸))
207206oveq2d 7410 . . . . . . . . . . 11 (𝑘 = 𝐸 → (( bday ‘𝐶) +no ( bday ‘𝑘)) = (( bday ‘𝐶) +no ( bday ‘𝐸)))
208207uneq1d 4159 . . . . . . . . . 10 (𝑘 = 𝐸 → ((( bday ‘𝐶) +no ( bday ‘𝑘)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) = ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))))
209206oveq2d 7410 . . . . . . . . . . 11 (𝑘 = 𝐸 → (( bday ‘𝐷) +no ( bday ‘𝑘)) = (( bday ‘𝐷) +no ( bday ‘𝐸)))
210209uneq2d 4160 . . . . . . . . . 10 (𝑘 = 𝐸 → ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑘))) = ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
211208, 210uneq12d 4161 . . . . . . . . 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 4160 . . . . . . . 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 2743 . . . . . . 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 5145 . . . . . . . . . 10 (𝑘 = 𝐸 → (𝑘 <s 𝑙 ↔ 𝐸 <s 𝑙))
215214anbi2d 629 . . . . . . . . 9 (𝑘 = 𝐸 → ((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙)))
216 oveq2 7402 . . . . . . . . . . 11 (𝑘 = 𝐸 → (𝐶 ·s 𝑘) = (𝐶 ·s 𝐸))
217216oveq2d 7410 . . . . . . . . . 10 (𝑘 = 𝐸 → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) = ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)))
218 oveq2 7402 . . . . . . . . . . 11 (𝑘 = 𝐸 → (𝐷 ·s 𝑘) = (𝐷 ·s 𝐸))
219218oveq2d 7410 . . . . . . . . . 10 (𝑘 = 𝐸 → ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)) = ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)))
220217, 219breq12d 5155 . . . . . . . . 9 (𝑘 = 𝐸 → (((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘)) ↔ ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸))))
221215, 220imbi12d 344 . . . . . . . 8 (𝑘 = 𝐸 → (((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝑘)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝑘))) ↔ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)))))
222221anbi2d 629 . . . . . . 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 344 . . . . . 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 6879 . . . . . . . . . . . 12 (𝑙 = 𝐹 → ( bday ‘𝑙) = ( bday ‘𝐹))
225224oveq2d 7410 . . . . . . . . . . 11 (𝑙 = 𝐹 → (( bday ‘𝐷) +no ( bday ‘𝑙)) = (( bday ‘𝐷) +no ( bday ‘𝐹)))
226225uneq2d 4160 . . . . . . . . . 10 (𝑙 = 𝐹 → ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝑙))) = ((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))))
227224oveq2d 7410 . . . . . . . . . . 11 (𝑙 = 𝐹 → (( bday ‘𝐶) +no ( bday ‘𝑙)) = (( bday ‘𝐶) +no ( bday ‘𝐹)))
228227uneq1d 4159 . . . . . . . . . 10 (𝑙 = 𝐹 → ((( bday ‘𝐶) +no ( bday ‘𝑙)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))) = ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))
229226, 228uneq12d 4161 . . . . . . . . 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 4160 . . . . . . . 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 2743 . . . . . . 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 5146 . . . . . . . . . 10 (𝑙 = 𝐹 → (𝐸 <s 𝑙 ↔ 𝐸 <s 𝐹))
233232anbi2d 629 . . . . . . . . 9 (𝑙 = 𝐹 → ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹)))
234 oveq2 7402 . . . . . . . . . . 11 (𝑙 = 𝐹 → (𝐶 ·s 𝑙) = (𝐶 ·s 𝐹))
235234oveq1d 7409 . . . . . . . . . 10 (𝑙 = 𝐹 → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)))
236 oveq2 7402 . . . . . . . . . . 11 (𝑙 = 𝐹 → (𝐷 ·s 𝑙) = (𝐷 ·s 𝐹))
237236oveq1d 7409 . . . . . . . . . 10 (𝑙 = 𝐹 → ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
238235, 237breq12d 5155 . . . . . . . . 9 (𝑙 = 𝐹 → (((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸)) ↔ ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸))))
239233, 238imbi12d 344 . . . . . . . 8 (𝑙 = 𝐹 → (((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) → ((𝐶 ·s 𝑙) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝑙) -s (𝐷 ·s 𝐸))) ↔ ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))))
240239anbi2d 629 . . . . . . 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 344 . . . . . 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 3628 . . . . 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 31 . . . 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 86 . . 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 3148 . 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
Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070   ∪ cun 3943   class class class wbr 5142  Oncon0 6354  ‘cfv 6533  (class class class)co 7394   +no cnadd 8649   No csur 27072   <s cslt 27073   bday cbday 27074   -s csubs 27424   ·s cmuls 27491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-ot 4632  df-uni 4903  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5568  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-se 5626  df-we 5627  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-1st 7959  df-2nd 7960  df-frecs 8250  df-wrecs 8281  df-recs 8355  df-1o 8450  df-2o 8451  df-nadd 8650  df-no 27075  df-slt 27076  df-bday 27077  df-sle 27177  df-sslt 27212  df-scut 27214  df-0s 27254  df-made 27271  df-old 27272  df-left 27274  df-right 27275  df-norec 27351  df-norec2 27362  df-adds 27373  df-negs 27425  df-subs 27426  df-muls 27492
This theorem is referenced by:  mulscutlem  27516  mulscl  27519  sltmul  27521
  Copyright terms: Public domain W3C validator