Metamath Proof Explorer

Theorem mulsproplem13

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