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

Theorem mulsproplem13 27513
Description: Lemma for surreal multiplication. Remove the restriction on 𝐶 and 𝐷 from mulsproplem12 27512. (Contributed by Scott Fenton, 5-Mar-2025.)
Hypotheses
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 𝑒))))))
mulsproplem.2 (𝜑𝐶 No )
mulsproplem.3 (𝜑𝐷 No )
mulsproplem.4 (𝜑𝐸 No )
mulsproplem.5 (𝜑𝐹 No )
mulsproplem.6 (𝜑𝐶 <s 𝐷)
mulsproplem.7 (𝜑𝐸 <s 𝐹)
mulsproplem13.1 (𝜑 → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
Assertion
Ref Expression
mulsproplem13 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓
Allowed substitution hints:   𝜑(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem mulsproplem13
Dummy variables 𝑔 𝑖 𝑗 𝑘 𝑙 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulsproplem.1 . . . 4 (𝜑 → ∀𝑎 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 𝑒))))))
21adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → ∀𝑎 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 𝑒))))))
3 mulsproplem.2 . . . 4 (𝜑𝐶 No )
43adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐶 No )
5 mulsproplem.3 . . . 4 (𝜑𝐷 No )
65adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐷 No )
7 mulsproplem.4 . . . 4 (𝜑𝐸 No )
87adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐸 No )
9 mulsproplem.5 . . . 4 (𝜑𝐹 No )
109adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐹 No )
11 mulsproplem.6 . . . 4 (𝜑𝐶 <s 𝐷)
1211adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐶 <s 𝐷)
13 mulsproplem.7 . . . 4 (𝜑𝐸 <s 𝐹)
1413adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → 𝐸 <s 𝐹)
15 simpr 485 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)))
16 mulsproplem13.1 . . . 4 (𝜑 → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
1716adantr 481 . . 3 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
182, 4, 6, 8, 10, 12, 14, 15, 17mulsproplem12 27512 . 2 ((𝜑 ∧ (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
193adantr 481 . . . 4 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → 𝐶 No )
205adantr 481 . . . 4 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → 𝐷 No )
21 simpr 485 . . . 4 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → ( bday 𝐶) = ( bday 𝐷))
2211adantr 481 . . . 4 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → 𝐶 <s 𝐷)
23 nodense 27124 . . . 4 (((𝐶 No 𝐷 No ) ∧ (( bday 𝐶) = ( bday 𝐷) ∧ 𝐶 <s 𝐷)) → ∃𝑥 No (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))
2419, 20, 21, 22, 23syl22anc 837 . . 3 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → ∃𝑥 No (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))
25 unidm 4149 . . . . . . . . . . . . . . . 16 (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))
26 unidm 4149 . . . . . . . . . . . . . . . 16 ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) = (( bday ‘ 0s ) +no ( bday ‘ 0s ))
27 bday0s 27258 . . . . . . . . . . . . . . . . . 18 ( bday ‘ 0s ) = ∅
2827, 27oveq12i 7406 . . . . . . . . . . . . . . . . 17 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no ∅)
29 0elon 6408 . . . . . . . . . . . . . . . . . 18 ∅ ∈ On
30 naddrid 8667 . . . . . . . . . . . . . . . . . 18 (∅ ∈ On → (∅ +no ∅) = ∅)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . 17 (∅ +no ∅) = ∅
3228, 31eqtri 2760 . . . . . . . . . . . . . . . 16 (( bday ‘ 0s ) +no ( bday ‘ 0s )) = ∅
3325, 26, 323eqtri 2764 . . . . . . . . . . . . . . 15 (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s )))) = ∅
3433uneq2i 4157 . . . . . . . . . . . . . 14 ((( bday 𝐶) +no ( bday 𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = ((( bday 𝐶) +no ( bday 𝐹)) ∪ ∅)
35 un0 4387 . . . . . . . . . . . . . 14 ((( bday 𝐶) +no ( bday 𝐹)) ∪ ∅) = (( bday 𝐶) +no ( bday 𝐹))
3634, 35eqtri 2760 . . . . . . . . . . . . 13 ((( bday 𝐶) +no ( bday 𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = (( bday 𝐶) +no ( bday 𝐹))
37 ssun1 4169 . . . . . . . . . . . . . . 15 (( bday 𝐶) +no ( bday 𝐹)) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))
38 ssun2 4170 . . . . . . . . . . . . . . 15 ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
3937, 38sstri 3988 . . . . . . . . . . . . . 14 (( bday 𝐶) +no ( bday 𝐹)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
40 ssun2 4170 . . . . . . . . . . . . . 14 (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
4139, 40sstri 3988 . . . . . . . . . . . . 13 (( bday 𝐶) +no ( bday 𝐹)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
4236, 41eqsstri 4013 . . . . . . . . . . . 12 ((( bday 𝐶) +no ( bday 𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
4342sseli 3975 . . . . . . . . . . 11 (((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
4443imim1i 63 . . . . . . . . . 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 𝐸))))) → ((𝑎 ·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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
45446ralimi 3127 . . . . . . . . 9 (∀𝑎 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
461, 45syl 17 . . . . . . . 8 (𝜑 → ∀𝑎 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
4746, 3, 9mulsproplem11 27511 . . . . . . 7 (𝜑 → (𝐶 ·s 𝐹) ∈ No )
4833uneq2i 4157 . . . . . . . . . . . . . 14 ((( bday 𝐶) +no ( bday 𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = ((( bday 𝐶) +no ( bday 𝐸)) ∪ ∅)
49 un0 4387 . . . . . . . . . . . . . 14 ((( bday 𝐶) +no ( bday 𝐸)) ∪ ∅) = (( bday 𝐶) +no ( bday 𝐸))
5048, 49eqtri 2760 . . . . . . . . . . . . 13 ((( bday 𝐶) +no ( bday 𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = (( bday 𝐶) +no ( bday 𝐸))
51 ssun1 4169 . . . . . . . . . . . . . . 15 (( bday 𝐶) +no ( bday 𝐸)) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹)))
52 ssun1 4169 . . . . . . . . . . . . . . 15 ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
5351, 52sstri 3988 . . . . . . . . . . . . . 14 (( bday 𝐶) +no ( bday 𝐸)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
5453, 40sstri 3988 . . . . . . . . . . . . 13 (( bday 𝐶) +no ( bday 𝐸)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
5550, 54eqsstri 4013 . . . . . . . . . . . 12 ((( bday 𝐶) +no ( bday 𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
5655sseli 3975 . . . . . . . . . . 11 (((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
5756imim1i 63 . . . . . . . . . 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 𝐸))))) → ((𝑎 ·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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
58576ralimi 3127 . . . . . . . . 9 (∀𝑎 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
591, 58syl 17 . . . . . . . 8 (𝜑 → ∀𝑎 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
6059, 3, 7mulsproplem11 27511 . . . . . . 7 (𝜑 → (𝐶 ·s 𝐸) ∈ No )
6147, 60subscld 27464 . . . . . 6 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
6261adantr 481 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) ∈ No )
6346adantr 481 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
64 simprr1 1221 . . . . . . . . 9 ((( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))) → ( bday 𝑥) ∈ ( bday 𝐶))
6564adantl 482 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝑥) ∈ ( bday 𝐶))
66 bdayelon 27207 . . . . . . . . 9 ( bday 𝐶) ∈ On
67 simprrl 779 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝑥 No )
68 oldbday 27324 . . . . . . . . 9 ((( bday 𝐶) ∈ On ∧ 𝑥 No ) → (𝑥 ∈ ( O ‘( bday 𝐶)) ↔ ( bday 𝑥) ∈ ( bday 𝐶)))
6966, 67, 68sylancr 587 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (𝑥 ∈ ( O ‘( bday 𝐶)) ↔ ( bday 𝑥) ∈ ( bday 𝐶)))
7065, 69mpbird 256 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝑥 ∈ ( O ‘( bday 𝐶)))
719adantr 481 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐹 No )
7263, 70, 71mulsproplem2 27502 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (𝑥 ·s 𝐹) ∈ No )
7359adantr 481 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
747adantr 481 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐸 No )
7573, 70, 74mulsproplem2 27502 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (𝑥 ·s 𝐸) ∈ No )
7672, 75subscld 27464 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)) ∈ No )
7733uneq2i 4157 . . . . . . . . . . . . . 14 ((( bday 𝐷) +no ( bday 𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = ((( bday 𝐷) +no ( bday 𝐹)) ∪ ∅)
78 un0 4387 . . . . . . . . . . . . . 14 ((( bday 𝐷) +no ( bday 𝐹)) ∪ ∅) = (( bday 𝐷) +no ( bday 𝐹))
7977, 78eqtri 2760 . . . . . . . . . . . . 13 ((( bday 𝐷) +no ( bday 𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = (( bday 𝐷) +no ( bday 𝐹))
80 ssun2 4170 . . . . . . . . . . . . . . 15 (( bday 𝐷) +no ( bday 𝐹)) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹)))
8180, 52sstri 3988 . . . . . . . . . . . . . 14 (( bday 𝐷) +no ( bday 𝐹)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
8281, 40sstri 3988 . . . . . . . . . . . . 13 (( bday 𝐷) +no ( bday 𝐹)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
8379, 82eqsstri 4013 . . . . . . . . . . . 12 ((( bday 𝐷) +no ( bday 𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
8483sseli 3975 . . . . . . . . . . 11 (((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐷) +no ( bday 𝐹)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
8584imim1i 63 . . . . . . . . . 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 𝐸))))) → ((𝑎 ·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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
86856ralimi 3127 . . . . . . . . 9 (∀𝑎 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
871, 86syl 17 . . . . . . . 8 (𝜑 → ∀𝑎 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
8887, 5, 9mulsproplem11 27511 . . . . . . 7 (𝜑 → (𝐷 ·s 𝐹) ∈ No )
8933uneq2i 4157 . . . . . . . . . . . . . 14 ((( bday 𝐷) +no ( bday 𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = ((( bday 𝐷) +no ( bday 𝐸)) ∪ ∅)
90 un0 4387 . . . . . . . . . . . . . 14 ((( bday 𝐷) +no ( bday 𝐸)) ∪ ∅) = (( bday 𝐷) +no ( bday 𝐸))
9189, 90eqtri 2760 . . . . . . . . . . . . 13 ((( bday 𝐷) +no ( bday 𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) = (( bday 𝐷) +no ( bday 𝐸))
92 ssun2 4170 . . . . . . . . . . . . . . 15 (( bday 𝐷) +no ( bday 𝐸)) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))
9392, 38sstri 3988 . . . . . . . . . . . . . 14 (( bday 𝐷) +no ( bday 𝐸)) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
9493, 40sstri 3988 . . . . . . . . . . . . 13 (( bday 𝐷) +no ( bday 𝐸)) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
9591, 94eqsstri 4013 . . . . . . . . . . . 12 ((( bday 𝐷) +no ( bday 𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
9695sseli 3975 . . . . . . . . . . 11 (((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐷) +no ( bday 𝐸)) ∪ (((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((( bday 𝑎) +no ( bday 𝑏)) ∪ (((( bday 𝑐) +no ( bday 𝑒)) ∪ (( bday 𝑑) +no ( bday 𝑓))) ∪ ((( bday 𝑐) +no ( bday 𝑓)) ∪ (( bday 𝑑) +no ( bday 𝑒))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
9796imim1i 63 . . . . . . . . . 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 𝐸))))) → ((𝑎 ·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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
98976ralimi 3127 . . . . . . . . 9 (∀𝑎 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
991, 98syl 17 . . . . . . . 8 (𝜑 → ∀𝑎 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
10099, 5, 7mulsproplem11 27511 . . . . . . 7 (𝜑 → (𝐷 ·s 𝐸) ∈ No )
10188, 100subscld 27464 . . . . . 6 (𝜑 → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
102101adantr 481 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)) ∈ No )
1031mulsproplemcbv 27500 . . . . . . . 8 (𝜑 → ∀𝑔 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 𝑘))))))
104103adantr 481 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝑘))))))
105 onelss 6396 . . . . . . . . . . . . . . . 16 (( bday 𝐶) ∈ On → (( bday 𝑥) ∈ ( bday 𝐶) → ( bday 𝑥) ⊆ ( bday 𝐶)))
10666, 65, 105mpsyl 68 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝑥) ⊆ ( bday 𝐶))
107 simprl 769 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝐶) = ( bday 𝐷))
108106, 107sseqtrd 4019 . . . . . . . . . . . . . 14 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝑥) ⊆ ( bday 𝐷))
109 bdayelon 27207 . . . . . . . . . . . . . . 15 ( bday 𝑥) ∈ On
110 bdayelon 27207 . . . . . . . . . . . . . . 15 ( bday 𝐷) ∈ On
111 bdayelon 27207 . . . . . . . . . . . . . . 15 ( bday 𝐹) ∈ On
112 naddss1 8673 . . . . . . . . . . . . . . 15 ((( bday 𝑥) ∈ On ∧ ( bday 𝐷) ∈ On ∧ ( bday 𝐹) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐷) ↔ (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐷) +no ( bday 𝐹))))
113109, 110, 111, 112mp3an 1461 . . . . . . . . . . . . . 14 (( bday 𝑥) ⊆ ( bday 𝐷) ↔ (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐷) +no ( bday 𝐹)))
114108, 113sylib 217 . . . . . . . . . . . . 13 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐷) +no ( bday 𝐹)))
115 unss2 4178 . . . . . . . . . . . . 13 ((( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐷) +no ( bday 𝐹)) → ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝑥) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
116114, 115syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝑥) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
117 bdayelon 27207 . . . . . . . . . . . . . . 15 ( bday 𝐸) ∈ On
118 naddss1 8673 . . . . . . . . . . . . . . 15 ((( bday 𝑥) ∈ On ∧ ( bday 𝐷) ∈ On ∧ ( bday 𝐸) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐷) ↔ (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐷) +no ( bday 𝐸))))
119109, 110, 117, 118mp3an 1461 . . . . . . . . . . . . . 14 (( bday 𝑥) ⊆ ( bday 𝐷) ↔ (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐷) +no ( bday 𝐸)))
120108, 119sylib 217 . . . . . . . . . . . . 13 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐷) +no ( bday 𝐸)))
121 unss2 4178 . . . . . . . . . . . . 13 ((( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐷) +no ( bday 𝐸)) → ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝑥) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
122120, 121syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝑥) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
123 unss12 4179 . . . . . . . . . . . 12 ((((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝑥) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∧ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝑥) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) → (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝑥) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝑥) +no ( bday 𝐸)))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
124116, 122, 123syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝐸)))))
125 unss2 4178 . . . . . . . . . . 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 𝐸)))) → ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝑥) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝑥) +no ( bday 𝐸))))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
126124, 125syl 17 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝐸))))))
127126sseld 3978 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝐸))))) → ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
128127imim1d 82 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝑘))))) → (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( 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 𝑘)))))))
129128ralimd6v 3208 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝑘))))) → ∀𝑔 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 𝑘)))))))
130104, 129mpd 15 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝑘))))))
1313adantr 481 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐶 No )
132 simprr2 1222 . . . . . . 7 ((( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))) → 𝐶 <s 𝑥)
133132adantl 482 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐶 <s 𝑥)
13413adantr 481 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐸 <s 𝐹)
13565olcd 872 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝐶) ∈ ( bday 𝑥) ∨ ( bday 𝑥) ∈ ( bday 𝐶)))
13616adantr 481 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝐸) ∈ ( bday 𝐹) ∨ ( bday 𝐹) ∈ ( bday 𝐸)))
137130, 131, 67, 74, 71, 133, 134, 135, 136mulsproplem12 27512 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)))
138 naddss1 8673 . . . . . . . . . . . . . . 15 ((( bday 𝑥) ∈ On ∧ ( bday 𝐶) ∈ On ∧ ( bday 𝐸) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐶) ↔ (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐶) +no ( bday 𝐸))))
139109, 66, 117, 138mp3an 1461 . . . . . . . . . . . . . 14 (( bday 𝑥) ⊆ ( bday 𝐶) ↔ (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐶) +no ( bday 𝐸)))
140106, 139sylib 217 . . . . . . . . . . . . 13 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐶) +no ( bday 𝐸)))
141 unss1 4176 . . . . . . . . . . . . 13 ((( bday 𝑥) +no ( bday 𝐸)) ⊆ (( bday 𝐶) +no ( bday 𝐸)) → ((( bday 𝑥) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
142140, 141syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((( bday 𝑥) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))))
143 naddss1 8673 . . . . . . . . . . . . . . 15 ((( bday 𝑥) ∈ On ∧ ( bday 𝐶) ∈ On ∧ ( bday 𝐹) ∈ On) → (( bday 𝑥) ⊆ ( bday 𝐶) ↔ (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐶) +no ( bday 𝐹))))
144109, 66, 111, 143mp3an 1461 . . . . . . . . . . . . . 14 (( bday 𝑥) ⊆ ( bday 𝐶) ↔ (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐶) +no ( bday 𝐹)))
145106, 144sylib 217 . . . . . . . . . . . . 13 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐶) +no ( bday 𝐹)))
146 unss1 4176 . . . . . . . . . . . . 13 ((( bday 𝑥) +no ( bday 𝐹)) ⊆ (( bday 𝐶) +no ( bday 𝐹)) → ((( bday 𝑥) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
147145, 146syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((( bday 𝑥) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))
148 unss12 4179 . . . . . . . . . . . 12 ((((( bday 𝑥) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ⊆ ((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∧ ((( bday 𝑥) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))) ⊆ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) → (((( bday 𝑥) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝑥) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))) ⊆ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))
149142, 147, 148syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝐸)))))
150 unss2 4178 . . . . . . . . . . 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 𝐸)))) → ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝑥) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝑥) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))) ⊆ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸))))))
151149, 150syl 17 . . . . . . . . . 10 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝐸))))))
152151sseld 3978 . . . . . . . . 9 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝐸))))) → ((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( bday 𝑗) +no ( bday 𝑙))) ∪ ((( bday 𝑖) +no ( bday 𝑙)) ∪ (( bday 𝑗) +no ( bday 𝑘))))) ∈ ((( bday 𝐴) +no ( bday 𝐵)) ∪ (((( bday 𝐶) +no ( bday 𝐸)) ∪ (( bday 𝐷) +no ( bday 𝐹))) ∪ ((( bday 𝐶) +no ( bday 𝐹)) ∪ (( bday 𝐷) +no ( bday 𝐸)))))))
153152imim1d 82 . . . . . . . 8 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝑘))))) → (((( bday 𝑔) +no ( bday )) ∪ (((( bday 𝑖) +no ( bday 𝑘)) ∪ (( 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 𝑘)))))))
154153ralimd6v 3208 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝑘))))) → ∀𝑔 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 𝑘)))))))
155104, 154mpd 15 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <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 𝑘))))))
1565adantr 481 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝐷 No )
157 simprr3 1223 . . . . . . 7 ((( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))) → 𝑥 <s 𝐷)
158157adantl 482 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → 𝑥 <s 𝐷)
15965, 107eleqtrd 2835 . . . . . . 7 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ( bday 𝑥) ∈ ( bday 𝐷))
160159orcd 871 . . . . . 6 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → (( bday 𝑥) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝑥)))
161155, 67, 156, 74, 71, 158, 134, 160, 136mulsproplem12 27512 . . . . 5 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝑥 ·s 𝐹) -s (𝑥 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
16262, 76, 102, 137, 161slttrd 27191 . . . 4 ((𝜑 ∧ (( bday 𝐶) = ( bday 𝐷) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷)))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
163162anassrs 468 . . 3 (((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) ∧ (𝑥 No ∧ (( bday 𝑥) ∈ ( bday 𝐶) ∧ 𝐶 <s 𝑥𝑥 <s 𝐷))) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
16424, 163rexlimddv 3161 . 2 ((𝜑 ∧ ( bday 𝐶) = ( bday 𝐷)) → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
16566onordi 6465 . . . . 5 Ord ( bday 𝐶)
166110onordi 6465 . . . . 5 Ord ( bday 𝐷)
167 ordtri3or 6386 . . . . 5 ((Ord ( bday 𝐶) ∧ Ord ( bday 𝐷)) → (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)))
168165, 166, 167mp2an 690 . . . 4 (( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶))
169 df-3or 1088 . . . . 5 ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ↔ ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷)) ∨ ( bday 𝐷) ∈ ( bday 𝐶)))
170 or32 924 . . . . 5 (((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷)) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ↔ ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ∨ ( bday 𝐶) = ( bday 𝐷)))
171169, 170bitri 274 . . . 4 ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐶) = ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ↔ ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ∨ ( bday 𝐶) = ( bday 𝐷)))
172168, 171mpbi 229 . . 3 ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ∨ ( bday 𝐶) = ( bday 𝐷))
173172a1i 11 . 2 (𝜑 → ((( bday 𝐶) ∈ ( bday 𝐷) ∨ ( bday 𝐷) ∈ ( bday 𝐶)) ∨ ( bday 𝐶) = ( bday 𝐷)))
17418, 164, 173mpjaodan 957 1 (𝜑 → ((𝐶 ·s 𝐹) -s (𝐶 ·s 𝐸)) <s ((𝐷 ·s 𝐹) -s (𝐷 ·s 𝐸)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  wral 3061  wrex 3070  cun 3943  wss 3945  c0 4319   class class class wbr 5142  Ord word 6353  Oncon0 6354  cfv 6533  (class class class)co 7394   +no cnadd 8649   No csur 27072   <s cslt 27073   bday cbday 27074   0s c0s 27252   O cold 27267   -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:  mulsproplem14  27514
  Copyright terms: Public domain W3C validator