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

Theorem mulsproplemcbv 27500
Description: Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025.)
Hypothesis
Ref Expression
mulsproplem.1 (𝜑 → ∀𝑎 No 𝑏 No 𝑐 No 𝑑 No 𝑒 No 𝑓 No (((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
Assertion
Ref Expression
mulsproplemcbv (𝜑 → ∀𝑔 No No 𝑖 No 𝑗 No 𝑘 No 𝑙 No (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐴,𝑔,,𝑖,𝑗,𝑘,𝑙,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑔,,𝑖,𝑗,𝑘,𝑙   𝐶,𝑔,,𝑖,𝑗,𝑘,𝑙   𝐷,𝑔,,𝑖,𝑗,𝑘,𝑙   𝑔,𝐸,,𝑖,𝑗,𝑘,𝑙   𝑔,𝐹,,𝑖,𝑗,𝑘,𝑙
Allowed substitution hints:   𝜑(𝑒,𝑓,𝑔,,𝑖,𝑗,𝑘,𝑎,𝑏,𝑐,𝑑,𝑙)

Proof of Theorem mulsproplemcbv
StepHypRef Expression
1 mulsproplem.1 . 2 (𝜑 → ∀𝑎 No 𝑏 No 𝑐 No 𝑑 No 𝑒 No 𝑓 No (((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
2 fveq2 6879 . . . . . . 7 (𝑎 = 𝑔 → ( bday 𝑎) = ( bday 𝑔))
32oveq1d 7409 . . . . . 6 (𝑎 = 𝑔 → (( bday 𝑎) +no ( bday 𝑏)) = (( bday 𝑔) +no ( bday 𝑏)))
43uneq1d 4159 . . . . 5 (𝑎 = 𝑔 → ((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) = ((( bday 𝑔) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))))
54eleq1d 2818 . . . 4 (𝑎 = 𝑔 → (((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) ↔ ((( bday 𝑔) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
6 oveq1 7401 . . . . . 6 (𝑎 = 𝑔 → (𝑎 ·s 𝑏) = (𝑔 ·s 𝑏))
76eleq1d 2818 . . . . 5 (𝑎 = 𝑔 → ((𝑎 ·s 𝑏) ∈ No ↔ (𝑔 ·s 𝑏) ∈ No ))
87anbi1d 630 . . . 4 (𝑎 = 𝑔 → (((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
95, 8imbi12d 344 . . 3 (𝑎 = 𝑔 → ((((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ (((( bday 𝑔) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
10 fveq2 6879 . . . . . . 7 (𝑏 = → ( bday 𝑏) = ( bday ))
1110oveq2d 7410 . . . . . 6 (𝑏 = → (( bday 𝑔) +no ( bday 𝑏)) = (( bday 𝑔) +no ( bday )))
1211uneq1d 4159 . . . . 5 (𝑏 = → ((( bday 𝑔) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) = ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))))
1312eleq1d 2818 . . . 4 (𝑏 = → (((( bday 𝑔) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) ↔ ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
14 oveq2 7402 . . . . . 6 (𝑏 = → (𝑔 ·s 𝑏) = (𝑔 ·s ))
1514eleq1d 2818 . . . . 5 (𝑏 = → ((𝑔 ·s 𝑏) ∈ No ↔ (𝑔 ·s ) ∈ No ))
1615anbi1d 630 . . . 4 (𝑏 = → (((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
1713, 16imbi12d 344 . . 3 (𝑏 = → ((((( bday 𝑔) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
18 fveq2 6879 . . . . . . . . 9 (𝑐 = 𝑖 → ( bday 𝑐) = ( bday 𝑖))
1918oveq1d 7409 . . . . . . . 8 (𝑐 = 𝑖 → (( bday 𝑐) +no ( bday 𝑒)) = (( bday 𝑖) +no ( bday 𝑒)))
2019uneq1d 4159 . . . . . . 7 (𝑐 = 𝑖 → ((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) = ((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))))
2118oveq1d 7409 . . . . . . . 8 (𝑐 = 𝑖 → (( bday 𝑐) +no ( bday 𝑓)) = (( bday 𝑖) +no ( bday 𝑓)))
2221uneq1d 4159 . . . . . . 7 (𝑐 = 𝑖 → ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))) = ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))
2320, 22uneq12d 4161 . . . . . 6 (𝑐 = 𝑖 → (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒)))) = (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒)))))
2423uneq2d 4160 . . . . 5 (𝑐 = 𝑖 → ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) = ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))))
2524eleq1d 2818 . . . 4 (𝑐 = 𝑖 → (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) ↔ ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
26 breq1 5145 . . . . . . 7 (𝑐 = 𝑖 → (𝑐 <s 𝑑𝑖 <s 𝑑))
2726anbi1d 630 . . . . . 6 (𝑐 = 𝑖 → ((𝑐 <s 𝑑𝑒 <s 𝑓) ↔ (𝑖 <s 𝑑𝑒 <s 𝑓)))
28 oveq1 7401 . . . . . . . 8 (𝑐 = 𝑖 → (𝑐 ·s 𝑓) = (𝑖 ·s 𝑓))
29 oveq1 7401 . . . . . . . 8 (𝑐 = 𝑖 → (𝑐 ·s 𝑒) = (𝑖 ·s 𝑒))
3028, 29oveq12d 7412 . . . . . . 7 (𝑐 = 𝑖 → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)))
3130breq1d 5152 . . . . . 6 (𝑐 = 𝑖 → (((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))
3227, 31imbi12d 344 . . . . 5 (𝑐 = 𝑖 → (((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑑𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))
3332anbi2d 629 . . . 4 (𝑐 = 𝑖 → (((𝑔 ·s ) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑑𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
3425, 33imbi12d 344 . . 3 (𝑐 = 𝑖 → ((((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑑𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
35 fveq2 6879 . . . . . . . . 9 (𝑑 = 𝑗 → ( bday 𝑑) = ( bday 𝑗))
3635oveq1d 7409 . . . . . . . 8 (𝑑 = 𝑗 → (( bday 𝑑) +no ( bday 𝑓)) = (( bday 𝑗) +no ( bday 𝑓)))
3736uneq2d 4160 . . . . . . 7 (𝑑 = 𝑗 → ((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) = ((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))))
3835oveq1d 7409 . . . . . . . 8 (𝑑 = 𝑗 → (( bday 𝑑) +no ( bday 𝑒)) = (( bday 𝑗) +no ( bday 𝑒)))
3938uneq2d 4160 . . . . . . 7 (𝑑 = 𝑗 → ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))) = ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒))))
4037, 39uneq12d 4161 . . . . . 6 (𝑑 = 𝑗 → (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒)))) = (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒)))))
4140uneq2d 4160 . . . . 5 (𝑑 = 𝑗 → ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) = ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒))))))
4241eleq1d 2818 . . . 4 (𝑑 = 𝑗 → (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) ↔ ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
43 breq2 5146 . . . . . . 7 (𝑑 = 𝑗 → (𝑖 <s 𝑑𝑖 <s 𝑗))
4443anbi1d 630 . . . . . 6 (𝑑 = 𝑗 → ((𝑖 <s 𝑑𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗𝑒 <s 𝑓)))
45 oveq1 7401 . . . . . . . 8 (𝑑 = 𝑗 → (𝑑 ·s 𝑓) = (𝑗 ·s 𝑓))
46 oveq1 7401 . . . . . . . 8 (𝑑 = 𝑗 → (𝑑 ·s 𝑒) = (𝑗 ·s 𝑒))
4745, 46oveq12d 7412 . . . . . . 7 (𝑑 = 𝑗 → ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))
4847breq2d 5154 . . . . . 6 (𝑑 = 𝑗 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))
4944, 48imbi12d 344 . . . . 5 (𝑑 = 𝑗 → (((𝑖 <s 𝑑𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑗𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))))
5049anbi2d 629 . . . 4 (𝑑 = 𝑗 → (((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑑𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))))
5142, 50imbi12d 344 . . 3 (𝑑 = 𝑗 → ((((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑑𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))))))
52 fveq2 6879 . . . . . . . . 9 (𝑒 = 𝑘 → ( bday 𝑒) = ( bday 𝑘))
5352oveq2d 7410 . . . . . . . 8 (𝑒 = 𝑘 → (( bday 𝑖) +no ( bday 𝑒)) = (( bday 𝑖) +no ( bday 𝑘)))
5453uneq1d 4159 . . . . . . 7 (𝑒 = 𝑘 → ((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) = ((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))))
5552oveq2d 7410 . . . . . . . 8 (𝑒 = 𝑘 → (( bday 𝑗) +no ( bday 𝑒)) = (( bday 𝑗) +no ( bday 𝑘)))
5655uneq2d 4160 . . . . . . 7 (𝑒 = 𝑘 → ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒))) = ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘))))
5754, 56uneq12d 4161 . . . . . 6 (𝑒 = 𝑘 → (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒)))) = (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘)))))
5857uneq2d 4160 . . . . 5 (𝑒 = 𝑘 → ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒))))) = ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘))))))
5958eleq1d 2818 . . . 4 (𝑒 = 𝑘 → (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) ↔ ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
60 breq1 5145 . . . . . . 7 (𝑒 = 𝑘 → (𝑒 <s 𝑓𝑘 <s 𝑓))
6160anbi2d 629 . . . . . 6 (𝑒 = 𝑘 → ((𝑖 <s 𝑗𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗𝑘 <s 𝑓)))
62 oveq2 7402 . . . . . . . 8 (𝑒 = 𝑘 → (𝑖 ·s 𝑒) = (𝑖 ·s 𝑘))
6362oveq2d 7410 . . . . . . 7 (𝑒 = 𝑘 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)))
64 oveq2 7402 . . . . . . . 8 (𝑒 = 𝑘 → (𝑗 ·s 𝑒) = (𝑗 ·s 𝑘))
6564oveq2d 7410 . . . . . . 7 (𝑒 = 𝑘 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))
6663, 65breq12d 5155 . . . . . 6 (𝑒 = 𝑘 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))
6761, 66imbi12d 344 . . . . 5 (𝑒 = 𝑘 → (((𝑖 <s 𝑗𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))) ↔ ((𝑖 <s 𝑗𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))))
6867anbi2d 629 . . . 4 (𝑒 = 𝑘 → (((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))) ↔ ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))))
6959, 68imbi12d 344 . . 3 (𝑒 = 𝑘 → ((((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑒)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))) ↔ (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))))))
70 fveq2 6879 . . . . . . . . 9 (𝑓 = 𝑙 → ( bday 𝑓) = ( bday 𝑙))
7170oveq2d 7410 . . . . . . . 8 (𝑓 = 𝑙 → (( bday 𝑗) +no ( bday 𝑓)) = (( bday 𝑗) +no ( bday 𝑙)))
7271uneq2d 4160 . . . . . . 7 (𝑓 = 𝑙 → ((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))) = ((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))))
7370oveq2d 7410 . . . . . . . 8 (𝑓 = 𝑙 → (( bday 𝑖) +no ( bday 𝑓)) = (( bday 𝑖) +no ( bday 𝑙)))
7473uneq1d 4159 . . . . . . 7 (𝑓 = 𝑙 → ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘))) = ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))
7572, 74uneq12d 4161 . . . . . 6 (𝑓 = 𝑙 → (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘)))) = (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘)))))
7675uneq2d 4160 . . . . 5 (𝑓 = 𝑙 → ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) = ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))))
7776eleq1d 2818 . . . 4 (𝑓 = 𝑙 → (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑓))) ∪ ((( bday 𝑖) +no ( bday 𝑓)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) ↔ ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
78 breq2 5146 . . . . . . 7 (𝑓 = 𝑙 → (𝑘 <s 𝑓𝑘 <s 𝑙))
7978anbi2d 629 . . . . . 6 (𝑓 = 𝑙 → ((𝑖 <s 𝑗𝑘 <s 𝑓) ↔ (𝑖 <s 𝑗𝑘 <s 𝑙)))
80 oveq2 7402 . . . . . . . 8 (𝑓 = 𝑙 → (𝑖 ·s 𝑓) = (𝑖 ·s 𝑙))
8180oveq1d 7409 . . . . . . 7 (𝑓 = 𝑙 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) = ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)))
82 oveq2 7402 . . . . . . . 8 (𝑓 = 𝑙 → (𝑗 ·s 𝑓) = (𝑗 ·s 𝑙))
8382oveq1d 7409 . . . . . . 7 (𝑓 = 𝑙 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) = ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))
8481, 83breq12d 5155 . . . . . 6 (𝑓 = 𝑙 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) ↔ ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))
8579, 84imbi12d 344 . . . . 5 (𝑓 = 𝑙 → (((𝑖 <s 𝑗𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))) ↔ ((𝑖 <s 𝑗𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))
8685anbi2d 629 . . . 4 (𝑓 = 𝑙 → (((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))) ↔ ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
8777, 86imbi12d 344 . . 3 (𝑓 = 𝑙 → ((((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( 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 𝑘)))))))
889, 17, 34, 51, 69, 87cbvral6vw 3242 . 2 (∀𝑎 No 𝑏 No 𝑐 No 𝑑 No 𝑒 No 𝑓 No (((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ ∀𝑔 No No 𝑖 No 𝑗 No 𝑘 No 𝑙 No (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
891, 88sylib 217 1 (𝜑 → ∀𝑔 No No 𝑖 No 𝑗 No 𝑘 No 𝑙 No (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) → ((𝑔 ·s ) ∈ No ∧ ((𝑖 <s 𝑗𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  wral 3061  cun 3943   class class class wbr 5142  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-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-iota 6485  df-fv 6541  df-ov 7397
This theorem is referenced by:  mulsproplem13  27513  mulsproplem14  27514
  Copyright terms: Public domain W3C validator