MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsprop Structured version   Visualization version   GIF version
Theorem mulsprop 28522
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 28144 . . . . 5 (bday‘𝐴) ∈ On
2 bdayon 28144 . . . . 5 (bday‘𝐵) ∈ On
3 naddcl 8690 . . . . 5 (((bday‘𝐴) ∈ On ∧ (bday‘𝐵) ∈ On) → ((bday‘𝐴) +no (bday‘𝐵)) ∈ On)
41, 2, 3mp2an 705 . . . 4 ((bday‘𝐴) +no (bday‘𝐵)) ∈ On
5 bdayon 28144 . . . . . . 7 (bday‘𝐶) ∈ On
6 bdayon 28144 . . . . . . 7 (bday‘𝐸) ∈ On
7 naddcl 8690 . . . . . . 7 (((bday‘𝐶) ∈ On ∧ (bday‘𝐸) ∈ On) → ((bday‘𝐶) +no (bday‘𝐸)) ∈ On)
85, 6, 7mp2an 705 . . . . . 6 ((bday‘𝐶) +no (bday‘𝐸)) ∈ On
9 bdayon 28144 . . . . . . 7 (bday‘𝐷) ∈ On
10 bdayon 28144 . . . . . . 7 (bday‘𝐹) ∈ On
11 naddcl 8690 . . . . . . 7 (((bday‘𝐷) ∈ On ∧ (bday‘𝐹) ∈ On) → ((bday‘𝐷) +no (bday‘𝐹)) ∈ On)
129, 10, 11mp2an 705 . . . . . 6 ((bday‘𝐷) +no (bday‘𝐹)) ∈ On
138, 12onun2i 6486 . . . . 5 (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∈ On
14 naddcl 8690 . . . . . . 7 (((bday‘𝐶) ∈ On ∧ (bday‘𝐹) ∈ On) → ((bday‘𝐶) +no (bday‘𝐹)) ∈ On)
155, 10, 14mp2an 705 . . . . . 6 ((bday‘𝐶) +no (bday‘𝐹)) ∈ On
16 naddcl 8690 . . . . . . 7 (((bday‘𝐷) ∈ On ∧ (bday‘𝐸) ∈ On) → ((bday‘𝐷) +no (bday‘𝐸)) ∈ On)
179, 6, 16mp2an 705 . . . . . 6 ((bday‘𝐷) +no (bday‘𝐸)) ∈ On
1815, 17onun2i 6486 . . . . 5 (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))) ∈ On
1913, 18onun2i 6486 . . . 4 ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸)))) ∈ On
204, 19onun2i 6486 . . 3 (((bday‘𝐴) +no (bday‘𝐵)) ∪ ((((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))) ∪ (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))) ∈ On
21 risset 3237 . . 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 6886 . . . . . . . . . . . 12 (𝑎 = 𝑔 → (bday‘𝑎) = (bday‘𝑔))
2423oveq1d 7436 . . . . . . . . . . 11 (𝑎 = 𝑔 → ((bday‘𝑎) +no (bday‘𝑏)) = ((bday‘𝑔) +no (bday‘𝑏)))
2524uneq1d 4166 . . . . . . . . . 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 2771 . . . . . . . . 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 7428 . . . . . . . . . . 11 (𝑎 = 𝑔 → (𝑎 ·s 𝑏) = (𝑔 ·s 𝑏))
2827eleq1d 2845 . . . . . . . . . 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 6886 . . . . . . . . . . . 12 (𝑏 = ℎ → (bday‘𝑏) = (bday‘ℎ))
3231oveq2d 7437 . . . . . . . . . . 11 (𝑏 = ℎ → ((bday‘𝑔) +no (bday‘𝑏)) = ((bday‘𝑔) +no (bday‘ℎ)))
3332uneq1d 4166 . . . . . . . . . 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 2771 . . . . . . . . 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 7429 . . . . . . . . . . 11 (𝑏 = ℎ → (𝑔 ·s 𝑏) = (𝑔 ·s ℎ))
3635eleq1d 2845 . . . . . . . . . 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 6886 . . . . . . . . . . . . . 14 (𝑐 = 𝑖 → (bday‘𝑐) = (bday‘𝑖))
4039oveq1d 7436 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → ((bday‘𝑐) +no (bday‘𝑒)) = ((bday‘𝑖) +no (bday‘𝑒)))
4140uneq1d 4166 . . . . . . . . . . . 12 (𝑐 = 𝑖 → (((bday‘𝑐) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) = (((bday‘𝑖) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))))
4239oveq1d 7436 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → ((bday‘𝑐) +no (bday‘𝑓)) = ((bday‘𝑖) +no (bday‘𝑓)))
4342uneq1d 4166 . . . . . . . . . . . 12 (𝑐 = 𝑖 → (((bday‘𝑐) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))) = (((bday‘𝑖) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))))
4441, 43uneq12d 4168 . . . . . . . . . . 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 4167 . . . . . . . . . 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 2771 . . . . . . . . 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 5105 . . . . . . . . . . . 12 (𝑐 = 𝑖 → (𝑐 <s 𝑑 ↔ 𝑖 <s 𝑑))
4847anbi1d 643 . . . . . . . . . . 11 (𝑐 = 𝑖 → ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓)))
49 oveq1 7428 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (𝑐 ·s 𝑓) = (𝑖 ·s 𝑓))
50 oveq1 7428 . . . . . . . . . . . . 13 (𝑐 = 𝑖 → (𝑐 ·s 𝑒) = (𝑖 ·s 𝑒))
5149, 50oveq12d 7439 . . . . . . . . . . . 12 (𝑐 = 𝑖 → ((𝑐 ·s 𝑓) −s (𝑐 ·s 𝑒)) = ((𝑖 ·s 𝑓) −s (𝑖 ·s 𝑒)))
5251breq1d 5112 . . . . . . . . . . 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 6886 . . . . . . . . . . . . . 14 (𝑑 = 𝑗 → (bday‘𝑑) = (bday‘𝑗))
5756oveq1d 7436 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → ((bday‘𝑑) +no (bday‘𝑓)) = ((bday‘𝑗) +no (bday‘𝑓)))
5857uneq2d 4167 . . . . . . . . . . . 12 (𝑑 = 𝑗 → (((bday‘𝑖) +no (bday‘𝑒)) ∪ ((bday‘𝑑) +no (bday‘𝑓))) = (((bday‘𝑖) +no (bday‘𝑒)) ∪ ((bday‘𝑗) +no (bday‘𝑓))))
5956oveq1d 7436 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → ((bday‘𝑑) +no (bday‘𝑒)) = ((bday‘𝑗) +no (bday‘𝑒)))
6059uneq2d 4167 . . . . . . . . . . . 12 (𝑑 = 𝑗 → (((bday‘𝑖) +no (bday‘𝑓)) ∪ ((bday‘𝑑) +no (bday‘𝑒))) = (((bday‘𝑖) +no (bday‘𝑓)) ∪ ((bday‘𝑗) +no (bday‘𝑒))))
6158, 60uneq12d 4168 . . . . . . . . . . 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 4167 . . . . . . . . . 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 2771 . . . . . . . . 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 5106 . . . . . . . . . . . 12 (𝑑 = 𝑗 → (𝑖 <s 𝑑 ↔ 𝑖 <s 𝑗))
6564anbi1d 643 . . . . . . . . . . 11 (𝑑 = 𝑗 → ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓)))
66 oveq1 7428 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (𝑑 ·s 𝑓) = (𝑗 ·s 𝑓))
67 oveq1 7428 . . . . . . . . . . . . 13 (𝑑 = 𝑗 → (𝑑 ·s 𝑒) = (𝑗 ·s 𝑒))
6866, 67oveq12d 7439 . . . . . . . . . . . 12 (𝑑 = 𝑗 → ((𝑑 ·s 𝑓) −s (𝑑 ·s 𝑒)) = ((𝑗 ·s 𝑓) −s (𝑗 ·s 𝑒)))
6968breq2d 5114 . . . . . . . . . . 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 6886 . . . . . . . . . . . . . 14 (𝑒 = 𝑘 → (bday‘𝑒) = (bday‘𝑘))
7473oveq2d 7437 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → ((bday‘𝑖) +no (bday‘𝑒)) = ((bday‘𝑖) +no (bday‘𝑘)))
7574uneq1d 4166 . . . . . . . . . . . 12 (𝑒 = 𝑘 → (((bday‘𝑖) +no (bday‘𝑒)) ∪ ((bday‘𝑗) +no (bday‘𝑓))) = (((bday‘𝑖) +no (bday‘𝑘)) ∪ ((bday‘𝑗) +no (bday‘𝑓))))
7673oveq2d 7437 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → ((bday‘𝑗) +no (bday‘𝑒)) = ((bday‘𝑗) +no (bday‘𝑘)))
7776uneq2d 4167 . . . . . . . . . . . 12 (𝑒 = 𝑘 → (((bday‘𝑖) +no (bday‘𝑓)) ∪ ((bday‘𝑗) +no (bday‘𝑒))) = (((bday‘𝑖) +no (bday‘𝑓)) ∪ ((bday‘𝑗) +no (bday‘𝑘))))
7875, 77uneq12d 4168 . . . . . . . . . . 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 4167 . . . . . . . . . 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 2771 . . . . . . . . 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 5105 . . . . . . . . . . . 12 (𝑒 = 𝑘 → (𝑒 <s 𝑓 ↔ 𝑘 <s 𝑓))
8281anbi2d 642 . . . . . . . . . . 11 (𝑒 = 𝑘 → ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓)))
83 oveq2 7429 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (𝑖 ·s 𝑒) = (𝑖 ·s 𝑘))
8483oveq2d 7437 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((𝑖 ·s 𝑓) −s (𝑖 ·s 𝑒)) = ((𝑖 ·s 𝑓) −s (𝑖 ·s 𝑘)))
85 oveq2 7429 . . . . . . . . . . . . 13 (𝑒 = 𝑘 → (𝑗 ·s 𝑒) = (𝑗 ·s 𝑘))
8685oveq2d 7437 . . . . . . . . . . . 12 (𝑒 = 𝑘 → ((𝑗 ·s 𝑓) −s (𝑗 ·s 𝑒)) = ((𝑗 ·s 𝑓) −s (𝑗 ·s 𝑘)))
8784, 86breq12d 5115 . . . . . . . . . . 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 6886 . . . . . . . . . . . . . 14 (𝑓 = 𝑙 → (bday‘𝑓) = (bday‘𝑙))
9291oveq2d 7437 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → ((bday‘𝑗) +no (bday‘𝑓)) = ((bday‘𝑗) +no (bday‘𝑙)))
9392uneq2d 4167 . . . . . . . . . . . 12 (𝑓 = 𝑙 → (((bday‘𝑖) +no (bday‘𝑘)) ∪ ((bday‘𝑗) +no (bday‘𝑓))) = (((bday‘𝑖) +no (bday‘𝑘)) ∪ ((bday‘𝑗) +no (bday‘𝑙))))
9491oveq2d 7437 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → ((bday‘𝑖) +no (bday‘𝑓)) = ((bday‘𝑖) +no (bday‘𝑙)))
9594uneq1d 4166 . . . . . . . . . . . 12 (𝑓 = 𝑙 → (((bday‘𝑖) +no (bday‘𝑓)) ∪ ((bday‘𝑗) +no (bday‘𝑘))) = (((bday‘𝑖) +no (bday‘𝑙)) ∪ ((bday‘𝑗) +no (bday‘𝑘))))
9693, 95uneq12d 4168 . . . . . . . . . . 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 4167 . . . . . . . . . 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 2771 . . . . . . . . 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 5106 . . . . . . . . . . . 12 (𝑓 = 𝑙 → (𝑘 <s 𝑓 ↔ 𝑘 <s 𝑙))
10099anbi2d 642 . . . . . . . . . . 11 (𝑓 = 𝑙 → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)))
101 oveq2 7429 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (𝑖 ·s 𝑓) = (𝑖 ·s 𝑙))
102101oveq1d 7436 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((𝑖 ·s 𝑓) −s (𝑖 ·s 𝑘)) = ((𝑖 ·s 𝑙) −s (𝑖 ·s 𝑘)))
103 oveq2 7429 . . . . . . . . . . . . 13 (𝑓 = 𝑙 → (𝑗 ·s 𝑓) = (𝑗 ·s 𝑙))
104103oveq1d 7436 . . . . . . . . . . . 12 (𝑓 = 𝑙 → ((𝑗 ·s 𝑓) −s (𝑗 ·s 𝑘)) = ((𝑗 ·s 𝑙) −s (𝑗 ·s 𝑘)))
105102, 104breq12d 5115 . . . . . . . . . . 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 3248 . . . . . . 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 2764 . . . . . . . . 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 3231 . . . . . . 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 3316 . . . . . . . . . . . . . 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 3293 . . . . . . . . . . . . . . 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 3293 . . . . . . . . . . . . . . . . 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 3293 . . . . . . . . . . . . . . . . . . 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 3189 . . . . . . . . . . . . . . . . . . . . 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 3237 . . . . . . . . . . . . . . . . . . . . . 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 3137 . . . . . . . . . . . . . . . . . . 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 3137 . . . . . . . . . . . . . . . . 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 3137 . . . . . . . . . . . . . . 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 28518 . . . . . . . . . . . . . . 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 28521 . . . . . . . . . . . . . . . 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 3208 . . . . . . . 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 3208 . . . . . . 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 7869 . . . . 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 6886 . . . . . . . . . 10 (𝑔 = 𝐴 → (bday‘𝑔) = (bday‘𝐴))
157156oveq1d 7436 . . . . . . . . 9 (𝑔 = 𝐴 → ((bday‘𝑔) +no (bday‘ℎ)) = ((bday‘𝐴) +no (bday‘ℎ)))
158157uneq1d 4166 . . . . . . . 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 2771 . . . . . . 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 7428 . . . . . . . . 9 (𝑔 = 𝐴 → (𝑔 ·s ℎ) = (𝐴 ·s ℎ))
161160eleq1d 2845 . . . . . . . 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 6886 . . . . . . . . . 10 (ℎ = 𝐵 → (bday‘ℎ) = (bday‘𝐵))
165164oveq2d 7437 . . . . . . . . 9 (ℎ = 𝐵 → ((bday‘𝐴) +no (bday‘ℎ)) = ((bday‘𝐴) +no (bday‘𝐵)))
166165uneq1d 4166 . . . . . . . 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 2771 . . . . . . 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 7429 . . . . . . . . 9 (ℎ = 𝐵 → (𝐴 ·s ℎ) = (𝐴 ·s 𝐵))
169168eleq1d 2845 . . . . . . . 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 6886 . . . . . . . . . . . 12 (𝑖 = 𝐶 → (bday‘𝑖) = (bday‘𝐶))
173172oveq1d 7436 . . . . . . . . . . 11 (𝑖 = 𝐶 → ((bday‘𝑖) +no (bday‘𝑘)) = ((bday‘𝐶) +no (bday‘𝑘)))
174173uneq1d 4166 . . . . . . . . . 10 (𝑖 = 𝐶 → (((bday‘𝑖) +no (bday‘𝑘)) ∪ ((bday‘𝑗) +no (bday‘𝑙))) = (((bday‘𝐶) +no (bday‘𝑘)) ∪ ((bday‘𝑗) +no (bday‘𝑙))))
175172oveq1d 7436 . . . . . . . . . . 11 (𝑖 = 𝐶 → ((bday‘𝑖) +no (bday‘𝑙)) = ((bday‘𝐶) +no (bday‘𝑙)))
176175uneq1d 4166 . . . . . . . . . 10 (𝑖 = 𝐶 → (((bday‘𝑖) +no (bday‘𝑙)) ∪ ((bday‘𝑗) +no (bday‘𝑘))) = (((bday‘𝐶) +no (bday‘𝑙)) ∪ ((bday‘𝑗) +no (bday‘𝑘))))
177174, 176uneq12d 4168 . . . . . . . . 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 4167 . . . . . . . 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 2771 . . . . . . 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 5105 . . . . . . . . . 10 (𝑖 = 𝐶 → (𝑖 <s 𝑗 ↔ 𝐶 <s 𝑗))
181180anbi1d 643 . . . . . . . . 9 (𝑖 = 𝐶 → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙)))
182 oveq1 7428 . . . . . . . . . . 11 (𝑖 = 𝐶 → (𝑖 ·s 𝑙) = (𝐶 ·s 𝑙))
183 oveq1 7428 . . . . . . . . . . 11 (𝑖 = 𝐶 → (𝑖 ·s 𝑘) = (𝐶 ·s 𝑘))
184182, 183oveq12d 7439 . . . . . . . . . 10 (𝑖 = 𝐶 → ((𝑖 ·s 𝑙) −s (𝑖 ·s 𝑘)) = ((𝐶 ·s 𝑙) −s (𝐶 ·s 𝑘)))
185184breq1d 5112 . . . . . . . . 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 6886 . . . . . . . . . . . 12 (𝑗 = 𝐷 → (bday‘𝑗) = (bday‘𝐷))
190189oveq1d 7436 . . . . . . . . . . 11 (𝑗 = 𝐷 → ((bday‘𝑗) +no (bday‘𝑙)) = ((bday‘𝐷) +no (bday‘𝑙)))
191190uneq2d 4167 . . . . . . . . . 10 (𝑗 = 𝐷 → (((bday‘𝐶) +no (bday‘𝑘)) ∪ ((bday‘𝑗) +no (bday‘𝑙))) = (((bday‘𝐶) +no (bday‘𝑘)) ∪ ((bday‘𝐷) +no (bday‘𝑙))))
192189oveq1d 7436 . . . . . . . . . . 11 (𝑗 = 𝐷 → ((bday‘𝑗) +no (bday‘𝑘)) = ((bday‘𝐷) +no (bday‘𝑘)))
193192uneq2d 4167 . . . . . . . . . 10 (𝑗 = 𝐷 → (((bday‘𝐶) +no (bday‘𝑙)) ∪ ((bday‘𝑗) +no (bday‘𝑘))) = (((bday‘𝐶) +no (bday‘𝑙)) ∪ ((bday‘𝐷) +no (bday‘𝑘))))
194191, 193uneq12d 4168 . . . . . . . . 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 4167 . . . . . . . 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 2771 . . . . . . 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 5106 . . . . . . . . . 10 (𝑗 = 𝐷 → (𝐶 <s 𝑗 ↔ 𝐶 <s 𝐷))
198197anbi1d 643 . . . . . . . . 9 (𝑗 = 𝐷 → ((𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙)))
199 oveq1 7428 . . . . . . . . . . 11 (𝑗 = 𝐷 → (𝑗 ·s 𝑙) = (𝐷 ·s 𝑙))
200 oveq1 7428 . . . . . . . . . . 11 (𝑗 = 𝐷 → (𝑗 ·s 𝑘) = (𝐷 ·s 𝑘))
201199, 200oveq12d 7439 . . . . . . . . . 10 (𝑗 = 𝐷 → ((𝑗 ·s 𝑙) −s (𝑗 ·s 𝑘)) = ((𝐷 ·s 𝑙) −s (𝐷 ·s 𝑘)))
202201breq2d 5114 . . . . . . . . 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 6886 . . . . . . . . . . . 12 (𝑘 = 𝐸 → (bday‘𝑘) = (bday‘𝐸))
207206oveq2d 7437 . . . . . . . . . . 11 (𝑘 = 𝐸 → ((bday‘𝐶) +no (bday‘𝑘)) = ((bday‘𝐶) +no (bday‘𝐸)))
208207uneq1d 4166 . . . . . . . . . 10 (𝑘 = 𝐸 → (((bday‘𝐶) +no (bday‘𝑘)) ∪ ((bday‘𝐷) +no (bday‘𝑙))) = (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝑙))))
209206oveq2d 7437 . . . . . . . . . . 11 (𝑘 = 𝐸 → ((bday‘𝐷) +no (bday‘𝑘)) = ((bday‘𝐷) +no (bday‘𝐸)))
210209uneq2d 4167 . . . . . . . . . 10 (𝑘 = 𝐸 → (((bday‘𝐶) +no (bday‘𝑙)) ∪ ((bday‘𝐷) +no (bday‘𝑘))) = (((bday‘𝐶) +no (bday‘𝑙)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
211208, 210uneq12d 4168 . . . . . . . . 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 4167 . . . . . . . 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 2771 . . . . . . 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 5105 . . . . . . . . . 10 (𝑘 = 𝐸 → (𝑘 <s 𝑙 ↔ 𝐸 <s 𝑙))
215214anbi2d 642 . . . . . . . . 9 (𝑘 = 𝐸 → ((𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙)))
216 oveq2 7429 . . . . . . . . . . 11 (𝑘 = 𝐸 → (𝐶 ·s 𝑘) = (𝐶 ·s 𝐸))
217216oveq2d 7437 . . . . . . . . . 10 (𝑘 = 𝐸 → ((𝐶 ·s 𝑙) −s (𝐶 ·s 𝑘)) = ((𝐶 ·s 𝑙) −s (𝐶 ·s 𝐸)))
218 oveq2 7429 . . . . . . . . . . 11 (𝑘 = 𝐸 → (𝐷 ·s 𝑘) = (𝐷 ·s 𝐸))
219218oveq2d 7437 . . . . . . . . . 10 (𝑘 = 𝐸 → ((𝐷 ·s 𝑙) −s (𝐷 ·s 𝑘)) = ((𝐷 ·s 𝑙) −s (𝐷 ·s 𝐸)))
220217, 219breq12d 5115 . . . . . . . . 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 6886 . . . . . . . . . . . 12 (𝑙 = 𝐹 → (bday‘𝑙) = (bday‘𝐹))
225224oveq2d 7437 . . . . . . . . . . 11 (𝑙 = 𝐹 → ((bday‘𝐷) +no (bday‘𝑙)) = ((bday‘𝐷) +no (bday‘𝐹)))
226225uneq2d 4167 . . . . . . . . . 10 (𝑙 = 𝐹 → (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝑙))) = (((bday‘𝐶) +no (bday‘𝐸)) ∪ ((bday‘𝐷) +no (bday‘𝐹))))
227224oveq2d 7437 . . . . . . . . . . 11 (𝑙 = 𝐹 → ((bday‘𝐶) +no (bday‘𝑙)) = ((bday‘𝐶) +no (bday‘𝐹)))
228227uneq1d 4166 . . . . . . . . . 10 (𝑙 = 𝐹 → (((bday‘𝐶) +no (bday‘𝑙)) ∪ ((bday‘𝐷) +no (bday‘𝐸))) = (((bday‘𝐶) +no (bday‘𝐹)) ∪ ((bday‘𝐷) +no (bday‘𝐸))))
229226, 228uneq12d 4168 . . . . . . . . 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 4167 . . . . . . . 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 2771 . . . . . . 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 5106 . . . . . . . . . 10 (𝑙 = 𝐹 → (𝐸 <s 𝑙 ↔ 𝐸 <s 𝐹))
233232anbi2d 642 . . . . . . . . 9 (𝑙 = 𝐹 → ((𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙) ↔ (𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹)))
234 oveq2 7429 . . . . . . . . . . 11 (𝑙 = 𝐹 → (𝐶 ·s 𝑙) = (𝐶 ·s 𝐹))
235234oveq1d 7436 . . . . . . . . . 10 (𝑙 = 𝐹 → ((𝐶 ·s 𝑙) −s (𝐶 ·s 𝐸)) = ((𝐶 ·s 𝐹) −s (𝐶 ·s 𝐸)))
236 oveq2 7429 . . . . . . . . . . 11 (𝑙 = 𝐹 → (𝐷 ·s 𝑙) = (𝐷 ·s 𝐹))
237236oveq1d 7436 . . . . . . . . . 10 (𝑙 = 𝐹 → ((𝐷 ·s 𝑙) −s (𝐷 ·s 𝐸)) = ((𝐷 ·s 𝐹) −s (𝐷 ·s 𝐸)))
238235, 237breq12d 5115 . . . . . . . . 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 3596 . . . . 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 3156 . 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 1569   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086   ∪ cun 4149   class class class wbr 5102  Oncon0 6362  ‘cfv 6539  (class class class)co 7421   +no cnadd 8678  Nocsur 28003   <s clts 28004  bdaycbday 28005   −s csubs 28412   ·s cmuls 28498
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-ot 4858  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-1st 8002  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-1o 8480  df-2o 8481  df-nadd 8679  df-no 28006  df-lts 28007  df-bday 28008  df-les 28108  df-slts 28150  df-cuts 28152  df-0s 28199  df-made 28219  df-old 28220  df-left 28222  df-right 28223  df-norec 28330  df-norec2 28341  df-adds 28352  df-negs 28413  df-subs 28414  df-muls 28499
This theorem is used by:  mulcutlem  28523  mulscl  28526  ltmuls  28528
  Copyright terms: Public domain W3C validator