Metamath Proof Explorer

Theorem mulsproplem14

Description: Lemma for surreal multiplication. Finally, we remove the restriction on E and F from mulsproplem12 and mulsproplem13 . This completes the induction on surreal multiplication. mulsprop brings all this together technically. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses 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 𝐹 )
Assertion mulsproplem14 ( 𝜑 → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 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 𝑒 ) ) ) ) ) )
2 mulsproplem.2 ⊢ ( 𝜑 → 𝐶 ∈ No )
3 mulsproplem.3 ⊢ ( 𝜑 → 𝐷 ∈ No )
4 mulsproplem.4 ⊢ ( 𝜑 → 𝐸 ∈ No )
5 mulsproplem.5 ⊢ ( 𝜑 → 𝐹 ∈ No )
6 mulsproplem.6 ⊢ ( 𝜑 → 𝐶 <s 𝐷 )
7 mulsproplem.7 ⊢ ( 𝜑 → 𝐸 <s 𝐹 )
8 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 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 𝑒 ) ) ) ) ) )
9 2 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ) → 𝐶 ∈ No )
10 3 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ) → 𝐷 ∈ No )
11 4 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ) → 𝐸 ∈ No )
12 5 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ) → 𝐹 ∈ No )
13 6 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ) → 𝐶 <s 𝐷 )
14 7 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ) → 𝐸 <s 𝐹 )
15 simpr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ) → ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) )
16 8 9 10 11 12 13 14 15 mulsproplem13 ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) )
17 4 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) → 𝐸 ∈ No )
18 5 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) → 𝐹 ∈ No )
19 simpr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) → ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) )
20 7 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) → 𝐸 <s 𝐹 )
21 nodense ⊢ ( ( ( 𝐸 ∈ No ∧ 𝐹 ∈ No ) ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ 𝐸 <s 𝐹 ) ) → ∃ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) )
22 17 18 19 20 21 syl22anc ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) → ∃ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) )
23 unidm ⊢ ( ( ( ( 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 ) ) )
24 unidm ⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) )
25 bday0s ⊢ ( bday ‘ 0s ) = ∅
26 25 25 oveq12i ⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ( ∅ +no ∅ )
27 0elon ⊢ ∅ ∈ On
28 naddrid ⊢ ( ∅ ∈ On → ( ∅ +no ∅ ) = ∅ )
29 27 28 ax-mp ⊢ ( ∅ +no ∅ ) = ∅
30 26 29 eqtri ⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ∅
31 23 24 30 3eqtri ⊢ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) = ∅
32 31 uneq2i ⊢ ( ( ( 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 ‘ 𝐸 ) ) ∪ ∅ )
33 un0 ⊢ ( ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ∪ ∅ ) = ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) )
34 32 33 eqtri ⊢ ( ( ( 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 ssun2 ⊢ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) )
36 ssun2 ⊢ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
37 35 36 sstri ⊢ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
38 ssun2 ⊢ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ⊆ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) )
39 37 38 sstri ⊢ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ⊆ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) )
40 34 39 eqsstri ⊢ ( ( ( 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 ‘ 𝐸 ) ) ) ) )
41 40 sseli ⊢ ( ( ( ( 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 ‘ 𝐸 ) ) ) ) ) )
42 41 imim1i ⊢ ( ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
43 42 6ralimi ⊢ ( ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
44 1 43 syl ⊢ ( 𝜑 → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
45 44 3 4 mulsproplem11 ⊢ ( 𝜑 → ( 𝐷 ·s 𝐸 ) ∈ No )
46 31 uneq2i ⊢ ( ( ( 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 ‘ 𝐸 ) ) ∪ ∅ )
47 un0 ⊢ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ∅ ) = ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) )
48 46 47 eqtri ⊢ ( ( ( 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 ssun1 ⊢ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) )
50 ssun1 ⊢ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
51 49 50 sstri ⊢ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
52 51 38 sstri ⊢ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ⊆ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) )
53 48 52 eqsstri ⊢ ( ( ( 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 ‘ 𝐸 ) ) ) ) )
54 53 sseli ⊢ ( ( ( ( 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 ‘ 𝐸 ) ) ) ) ) )
55 54 imim1i ⊢ ( ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
56 55 6ralimi ⊢ ( ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
57 1 56 syl ⊢ ( 𝜑 → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
58 57 2 4 mulsproplem11 ⊢ ( 𝜑 → ( 𝐶 ·s 𝐸 ) ∈ No )
59 45 58 subscld ⊢ ( 𝜑 → ( ( 𝐷 ·s 𝐸 ) -s ( 𝐶 ·s 𝐸 ) ) ∈ No )
60 59 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐷 ·s 𝐸 ) -s ( 𝐶 ·s 𝐸 ) ) ∈ No )
61 44 adantr ⊢ ( ( 𝜑 ∧ ( ( 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 𝑒 ) ) ) ) ) )
62 3 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝐷 ∈ No )
63 simprr1 ⊢ ( ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) )
64 63 adantl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) )
65 bdayelon ⊢ ( bday ‘ 𝐸 ) ∈ On
66 simprrl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝑥 ∈ No )
67 oldbday ⊢ ( ( ( bday ‘ 𝐸 ) ∈ On ∧ 𝑥 ∈ No ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐸 ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ) )
68 65 66 67 sylancr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐸 ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ) )
69 64 68 mpbird ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝑥 ∈ ( O ‘ ( bday ‘ 𝐸 ) ) )
70 61 62 69 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( 𝐷 ·s 𝑥 ) ∈ No )
71 57 adantr ⊢ ( ( 𝜑 ∧ ( ( 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 𝑒 ) ) ) ) ) )
72 2 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝐶 ∈ No )
73 71 72 69 mulsproplem3 ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( 𝐶 ·s 𝑥 ) ∈ No )
74 70 73 subscld ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐷 ·s 𝑥 ) -s ( 𝐶 ·s 𝑥 ) ) ∈ No )
75 31 uneq2i ⊢ ( ( ( 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 ‘ 𝐹 ) ) ∪ ∅ )
76 un0 ⊢ ( ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ∪ ∅ ) = ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) )
77 75 76 eqtri ⊢ ( ( ( 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 ssun2 ⊢ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) )
79 78 50 sstri ⊢ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
80 79 38 sstri ⊢ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ⊆ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) )
81 77 80 eqsstri ⊢ ( ( ( 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 ‘ 𝐸 ) ) ) ) )
82 81 sseli ⊢ ( ( ( ( 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 ‘ 𝐸 ) ) ) ) ) )
83 82 imim1i ⊢ ( ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
84 83 6ralimi ⊢ ( ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
85 1 84 syl ⊢ ( 𝜑 → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
86 85 3 5 mulsproplem11 ⊢ ( 𝜑 → ( 𝐷 ·s 𝐹 ) ∈ No )
87 31 uneq2i ⊢ ( ( ( 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 ‘ 𝐹 ) ) ∪ ∅ )
88 un0 ⊢ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ∅ ) = ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) )
89 87 88 eqtri ⊢ ( ( ( 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 ssun1 ⊢ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) )
91 90 36 sstri ⊢ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
92 91 38 sstri ⊢ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ⊆ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) )
93 89 92 eqsstri ⊢ ( ( ( 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 ‘ 𝐸 ) ) ) ) )
94 93 sseli ⊢ ( ( ( ( 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 ‘ 𝐸 ) ) ) ) ) )
95 94 imim1i ⊢ ( ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
96 95 6ralimi ⊢ ( ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
97 1 96 syl ⊢ ( 𝜑 → ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) )
98 97 2 5 mulsproplem11 ⊢ ( 𝜑 → ( 𝐶 ·s 𝐹 ) ∈ No )
99 86 98 subscld ⊢ ( 𝜑 → ( ( 𝐷 ·s 𝐹 ) -s ( 𝐶 ·s 𝐹 ) ) ∈ No )
100 99 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐷 ·s 𝐹 ) -s ( 𝐶 ·s 𝐹 ) ) ∈ No )
101 1 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 𝑘 ) ) ) ) ) )
102 101 adantr ⊢ ( ( 𝜑 ∧ ( ( 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 𝑘 ) ) ) ) ) )
103 onelss ⊢ ( ( bday ‘ 𝐸 ) ∈ On → ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) → ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐸 ) ) )
104 65 64 103 mpsyl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐸 ) )
105 simprl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) )
106 104 105 sseqtrd ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐹 ) )
107 bdayelon ⊢ ( bday ‘ 𝑥 ) ∈ On
108 bdayelon ⊢ ( bday ‘ 𝐹 ) ∈ On
109 bdayelon ⊢ ( bday ‘ 𝐷 ) ∈ On
110 naddss2 ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( bday ‘ 𝐹 ) ∈ On ∧ ( bday ‘ 𝐷 ) ∈ On ) → ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐹 ) ↔ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) )
111 107 108 109 110 mp3an ⊢ ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐹 ) ↔ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) )
112 106 111 sylib ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) )
113 unss2 ⊢ ( ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) )
114 112 113 syl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) )
115 bdayelon ⊢ ( bday ‘ 𝐶 ) ∈ On
116 naddss2 ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( bday ‘ 𝐹 ) ∈ On ∧ ( bday ‘ 𝐶 ) ∈ On ) → ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐹 ) ↔ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ) )
117 107 108 115 116 mp3an ⊢ ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐹 ) ↔ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) )
118 106 117 sylib ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) )
119 unss1 ⊢ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
120 118 119 syl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
121 unss12 ⊢ ( ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∧ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) → ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) )
122 114 120 121 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 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 ‘ 𝐸 ) ) ) ) )
123 unss2 ⊢ ( ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ⊆ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
124 122 123 syl ⊢ ( ( 𝜑 ∧ ( ( 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 ‘ 𝐸 ) ) ) ) ) )
125 124 sseld ⊢ ( ( 𝜑 ∧ ( ( 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 ‘ 𝐸 ) ) ) ) ) ) )
126 125 imim1d ⊢ ( ( 𝜑 ∧ ( ( 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 𝑘 ) ) ) ) ) ) )
127 126 ralimd6v ⊢ ( ( 𝜑 ∧ ( ( 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 𝑘 ) ) ) ) ) ) )
128 102 127 mpd ⊢ ( ( 𝜑 ∧ ( ( 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 𝑘 ) ) ) ) ) )
129 4 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝐸 ∈ No )
130 6 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝐶 <s 𝐷 )
131 simprr2 ⊢ ( ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) → 𝐸 <s 𝑥 )
132 131 adantl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝐸 <s 𝑥 )
133 64 olcd ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝑥 ) ∨ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ) )
134 128 72 62 129 66 130 132 133 mulsproplem13 ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐶 ·s 𝑥 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑥 ) -s ( 𝐷 ·s 𝐸 ) ) )
135 45 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( 𝐷 ·s 𝐸 ) ∈ No )
136 58 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( 𝐶 ·s 𝐸 ) ∈ No )
137 135 70 136 73 sltsubsub3bd ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( ( 𝐷 ·s 𝐸 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑥 ) -s ( 𝐶 ·s 𝑥 ) ) ↔ ( ( 𝐶 ·s 𝑥 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑥 ) -s ( 𝐷 ·s 𝐸 ) ) ) )
138 134 137 mpbird ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐷 ·s 𝐸 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑥 ) -s ( 𝐶 ·s 𝑥 ) ) )
139 naddss2 ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( bday ‘ 𝐸 ) ∈ On ∧ ( bday ‘ 𝐶 ) ∈ On ) → ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐸 ) ↔ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ) )
140 107 65 115 139 mp3an ⊢ ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐸 ) ↔ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) )
141 104 140 sylib ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) )
142 unss1 ⊢ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) )
143 141 142 syl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) )
144 naddss2 ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( bday ‘ 𝐸 ) ∈ On ∧ ( bday ‘ 𝐷 ) ∈ On ) → ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐸 ) ↔ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
145 107 65 109 144 mp3an ⊢ ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝐸 ) ↔ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) )
146 104 145 sylib ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) )
147 unss2 ⊢ ( ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ⊆ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
148 146 147 syl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
149 unss12 ⊢ ( ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∧ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ⊆ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) → ( ( ( ( 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 143 148 149 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 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 ‘ 𝐸 ) ) ) ) )
151 unss2 ⊢ ( ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ) ⊆ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑥 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑥 ) ) ) ) ) ⊆ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
152 150 151 syl ⊢ ( ( 𝜑 ∧ ( ( 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 ‘ 𝐸 ) ) ) ) ) )
153 152 sseld ⊢ ( ( 𝜑 ∧ ( ( 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 ‘ 𝐸 ) ) ) ) ) ) )
154 153 imim1d ⊢ ( ( 𝜑 ∧ ( ( 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 𝑘 ) ) ) ) ) ) )
155 154 ralimd6v ⊢ ( ( 𝜑 ∧ ( ( 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 𝑘 ) ) ) ) ) ) )
156 102 155 mpd ⊢ ( ( 𝜑 ∧ ( ( 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 𝑘 ) ) ) ) ) )
157 5 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝐹 ∈ No )
158 simprr3 ⊢ ( ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) → 𝑥 <s 𝐹 )
159 158 adantl ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → 𝑥 <s 𝐹 )
160 64 105 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐹 ) )
161 160 orcd ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝑥 ) ) )
162 156 72 62 66 157 130 159 161 mulsproplem13 ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝑥 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝑥 ) ) )
163 86 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( 𝐷 ·s 𝐹 ) ∈ No )
164 98 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( 𝐶 ·s 𝐹 ) ∈ No )
165 70 163 73 164 sltsubsub3bd ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( ( 𝐷 ·s 𝑥 ) -s ( 𝐶 ·s 𝑥 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐶 ·s 𝐹 ) ) ↔ ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝑥 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝑥 ) ) ) )
166 162 165 mpbird ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐷 ·s 𝑥 ) -s ( 𝐶 ·s 𝑥 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐶 ·s 𝐹 ) ) )
167 60 74 100 138 166 slttrd ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐷 ·s 𝐸 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐶 ·s 𝐹 ) ) )
168 45 86 58 98 sltsubsub3bd ⊢ ( 𝜑 → ( ( ( 𝐷 ·s 𝐸 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐶 ·s 𝐹 ) ) ↔ ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( ( 𝐷 ·s 𝐸 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐶 ·s 𝐹 ) ) ↔ ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) )
170 167 169 mpbid ⊢ ( ( 𝜑 ∧ ( ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) )
171 170 anassrs ⊢ ( ( ( 𝜑 ∧ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) ∧ ( 𝑥 ∈ No ∧ ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐸 ) ∧ 𝐸 <s 𝑥 ∧ 𝑥 <s 𝐹 ) ) ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) )
172 22 171 rexlimddv ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) )
173 65 onordi ⊢ Ord ( bday ‘ 𝐸 )
174 108 onordi ⊢ Ord ( bday ‘ 𝐹 )
175 ordtri3or ⊢ ( ( Ord ( bday ‘ 𝐸 ) ∧ Ord ( bday ‘ 𝐹 ) ) → ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) )
176 173 174 175 mp2an ⊢ ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) )
177 df-3or ⊢ ( ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ↔ ( ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) )
178 or32 ⊢ ( ( ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ↔ ( ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) )
179 177 178 bitri ⊢ ( ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ↔ ( ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) )
180 176 179 mpbi ⊢ ( ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) )
181 180 a1i ⊢ ( 𝜑 → ( ( ( bday ‘ 𝐸 ) ∈ ( bday ‘ 𝐹 ) ∨ ( bday ‘ 𝐹 ) ∈ ( bday ‘ 𝐸 ) ) ∨ ( bday ‘ 𝐸 ) = ( bday ‘ 𝐹 ) ) )
182 16 172 181 mpjaodan ⊢ ( 𝜑 → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) )