Theorem mulsproplem1

Description: Lemma for surreal multiplication. Instantiate some variables. (Contributed by Scott Fenton, 4-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 𝑒 ) ) ) ) ) )
	mulsproplem1.1	⊢ ( 𝜑 → 𝑋 ∈ No )
	mulsproplem1.2	⊢ ( 𝜑 → 𝑌 ∈ No )
	mulsproplem1.3	⊢ ( 𝜑 → 𝑍 ∈ No )
	mulsproplem1.4	⊢ ( 𝜑 → 𝑊 ∈ No )
	mulsproplem1.5	⊢ ( 𝜑 → 𝑇 ∈ No )
	mulsproplem1.6	⊢ ( 𝜑 → 𝑈 ∈ No )
	mulsproplem1.7	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑈 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
Assertion	mulsproplem1	⊢ ( 𝜑 → ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈 ) → ( ( 𝑍 ·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		mulsproplem1.1	⊢ ( 𝜑 → 𝑋 ∈ No )
3		mulsproplem1.2	⊢ ( 𝜑 → 𝑌 ∈ No )
4		mulsproplem1.3	⊢ ( 𝜑 → 𝑍 ∈ No )
5		mulsproplem1.4	⊢ ( 𝜑 → 𝑊 ∈ No )
6		mulsproplem1.5	⊢ ( 𝜑 → 𝑇 ∈ No )
7		mulsproplem1.6	⊢ ( 𝜑 → 𝑈 ∈ No )
8		mulsproplem1.7	⊢ ( 𝜑 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑈 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
9		fveq2	⊢ ( 𝑎 = 𝑋 → ( bday ‘ 𝑎 ) = ( bday ‘ 𝑋 ) )
10	9	oveq1d	⊢ ( 𝑎 = 𝑋 → ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑏 ) ) )
11	10	uneq1d	⊢ ( 𝑎 = 𝑋 → ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) )
12	11	eleq1d	⊢ ( 𝑎 = 𝑋 → ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ) )
13		oveq1	⊢ ( 𝑎 = 𝑋 → ( 𝑎 ·s 𝑏 ) = ( 𝑋 ·s 𝑏 ) )
14	13	eleq1d	⊢ ( 𝑎 = 𝑋 → ( ( 𝑎 ·s 𝑏 ) ∈ No ↔ ( 𝑋 ·s 𝑏 ) ∈ No ) )
15	14	anbi1d	⊢ ( 𝑎 = 𝑋 → ( ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑋 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
16	12 15	imbi12d	⊢ ( 𝑎 = 𝑋 → ( ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) ) )
17		fveq2	⊢ ( 𝑏 = 𝑌 → ( bday ‘ 𝑏 ) = ( bday ‘ 𝑌 ) )
18	17	oveq2d	⊢ ( 𝑏 = 𝑌 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑏 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
19	18	uneq1d	⊢ ( 𝑏 = 𝑌 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) )
20	19	eleq1d	⊢ ( 𝑏 = 𝑌 → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ) )
21		oveq2	⊢ ( 𝑏 = 𝑌 → ( 𝑋 ·s 𝑏 ) = ( 𝑋 ·s 𝑌 ) )
22	21	eleq1d	⊢ ( 𝑏 = 𝑌 → ( ( 𝑋 ·s 𝑏 ) ∈ No ↔ ( 𝑋 ·s 𝑌 ) ∈ No ) )
23	22	anbi1d	⊢ ( 𝑏 = 𝑌 → ( ( ( 𝑋 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
24	20 23	imbi12d	⊢ ( 𝑏 = 𝑌 → ( ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) ) )
25		fveq2	⊢ ( 𝑐 = 𝑍 → ( bday ‘ 𝑐 ) = ( bday ‘ 𝑍 ) )
26	25	oveq1d	⊢ ( 𝑐 = 𝑍 → ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) = ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) )
27	26	uneq1d	⊢ ( 𝑐 = 𝑍 → ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) = ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) )
28	25	oveq1d	⊢ ( 𝑐 = 𝑍 → ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) = ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) )
29	28	uneq1d	⊢ ( 𝑐 = 𝑍 → ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) = ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) )
30	27 29	uneq12d	⊢ ( 𝑐 = 𝑍 → ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) = ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) )
31	30	uneq2d	⊢ ( 𝑐 = 𝑍 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) )
32	31	eleq1d	⊢ ( 𝑐 = 𝑍 → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ) )
33		breq1	⊢ ( 𝑐 = 𝑍 → ( 𝑐 <s 𝑑 ↔ 𝑍 <s 𝑑 ) )
34	33	anbi1d	⊢ ( 𝑐 = 𝑍 → ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) ↔ ( 𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓 ) ) )
35		oveq1	⊢ ( 𝑐 = 𝑍 → ( 𝑐 ·s 𝑓 ) = ( 𝑍 ·s 𝑓 ) )
36		oveq1	⊢ ( 𝑐 = 𝑍 → ( 𝑐 ·s 𝑒 ) = ( 𝑍 ·s 𝑒 ) )
37	35 36	oveq12d	⊢ ( 𝑐 = 𝑍 → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) = ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) )
38	37	breq1d	⊢ ( 𝑐 = 𝑍 → ( ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ↔ ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) )
39	34 38	imbi12d	⊢ ( 𝑐 = 𝑍 → ( ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ↔ ( ( 𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) )
40	39	anbi2d	⊢ ( 𝑐 = 𝑍 → ( ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
41	32 40	imbi12d	⊢ ( 𝑐 = 𝑍 → ( ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) ) )
42		fveq2	⊢ ( 𝑑 = 𝑊 → ( bday ‘ 𝑑 ) = ( bday ‘ 𝑊 ) )
43	42	oveq1d	⊢ ( 𝑑 = 𝑊 → ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) = ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) )
44	43	uneq2d	⊢ ( 𝑑 = 𝑊 → ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) = ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) )
45	42	oveq1d	⊢ ( 𝑑 = 𝑊 → ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) = ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) )
46	45	uneq2d	⊢ ( 𝑑 = 𝑊 → ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) = ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) ) )
47	44 46	uneq12d	⊢ ( 𝑑 = 𝑊 → ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) = ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) ) ) )
48	47	uneq2d	⊢ ( 𝑑 = 𝑊 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) ) ) ) )
49	48	eleq1d	⊢ ( 𝑑 = 𝑊 → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ) )
50		breq2	⊢ ( 𝑑 = 𝑊 → ( 𝑍 <s 𝑑 ↔ 𝑍 <s 𝑊 ) )
51	50	anbi1d	⊢ ( 𝑑 = 𝑊 → ( ( 𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓 ) ↔ ( 𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓 ) ) )
52		oveq1	⊢ ( 𝑑 = 𝑊 → ( 𝑑 ·s 𝑓 ) = ( 𝑊 ·s 𝑓 ) )
53		oveq1	⊢ ( 𝑑 = 𝑊 → ( 𝑑 ·s 𝑒 ) = ( 𝑊 ·s 𝑒 ) )
54	52 53	oveq12d	⊢ ( 𝑑 = 𝑊 → ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) = ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑒 ) ) )
55	54	breq2d	⊢ ( 𝑑 = 𝑊 → ( ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ↔ ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑒 ) ) ) )
56	51 55	imbi12d	⊢ ( 𝑑 = 𝑊 → ( ( ( 𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ↔ ( ( 𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑒 ) ) ) ) )
57	56	anbi2d	⊢ ( 𝑑 = 𝑊 → ( ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑒 ) ) ) ) ) )
58	49 57	imbi12d	⊢ ( 𝑑 = 𝑊 → ( ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) ) )
59		fveq2	⊢ ( 𝑒 = 𝑇 → ( bday ‘ 𝑒 ) = ( bday ‘ 𝑇 ) )
60	59	oveq2d	⊢ ( 𝑒 = 𝑇 → ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) = ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) )
61	60	uneq1d	⊢ ( 𝑒 = 𝑇 → ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) = ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) )
62	59	oveq2d	⊢ ( 𝑒 = 𝑇 → ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) = ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) )
63	62	uneq2d	⊢ ( 𝑒 = 𝑇 → ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) ) = ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) )
64	61 63	uneq12d	⊢ ( 𝑒 = 𝑇 → ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) ) ) = ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) ) )
65	64	uneq2d	⊢ ( 𝑒 = 𝑇 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) ) ) )
66	65	eleq1d	⊢ ( 𝑒 = 𝑇 → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ) )
67		breq1	⊢ ( 𝑒 = 𝑇 → ( 𝑒 <s 𝑓 ↔ 𝑇 <s 𝑓 ) )
68	67	anbi2d	⊢ ( 𝑒 = 𝑇 → ( ( 𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓 ) ↔ ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓 ) ) )
69		oveq2	⊢ ( 𝑒 = 𝑇 → ( 𝑍 ·s 𝑒 ) = ( 𝑍 ·s 𝑇 ) )
70	69	oveq2d	⊢ ( 𝑒 = 𝑇 → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) = ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑇 ) ) )
71		oveq2	⊢ ( 𝑒 = 𝑇 → ( 𝑊 ·s 𝑒 ) = ( 𝑊 ·s 𝑇 ) )
72	71	oveq2d	⊢ ( 𝑒 = 𝑇 → ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑒 ) ) = ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑇 ) ) )
73	70 72	breq12d	⊢ ( 𝑒 = 𝑇 → ( ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑒 ) ) ↔ ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑇 ) ) ) )
74	68 73	imbi12d	⊢ ( 𝑒 = 𝑇 → ( ( ( 𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑒 ) ) ) ↔ ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑇 ) ) ) ) )
75	74	anbi2d	⊢ ( 𝑒 = 𝑇 → ( ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑊 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑒 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑇 ) ) ) ) ) )
76	66 75	imbi12d	⊢ ( 𝑒 = 𝑇 → ( ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑇 ) ) ) ) ) ) )
77		fveq2	⊢ ( 𝑓 = 𝑈 → ( bday ‘ 𝑓 ) = ( bday ‘ 𝑈 ) )
78	77	oveq2d	⊢ ( 𝑓 = 𝑈 → ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) = ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑈 ) ) )
79	78	uneq2d	⊢ ( 𝑓 = 𝑈 → ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) = ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑈 ) ) ) )
80	77	oveq2d	⊢ ( 𝑓 = 𝑈 → ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) = ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑈 ) ) )
81	80	uneq1d	⊢ ( 𝑓 = 𝑈 → ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) = ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) )
82	79 81	uneq12d	⊢ ( 𝑓 = 𝑈 → ( ( ( ( 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	uneq2d	⊢ ( 𝑓 = 𝑈 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑈 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑈 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) ) ) )
84	83	eleq1d	⊢ ( 𝑓 = 𝑈 → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑊 ) +no ( bday ‘ 𝑇 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( 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		breq2	⊢ ( 𝑓 = 𝑈 → ( 𝑇 <s 𝑓 ↔ 𝑇 <s 𝑈 ) )
86	85	anbi2d	⊢ ( 𝑓 = 𝑈 → ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓 ) ↔ ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈 ) ) )
87		oveq2	⊢ ( 𝑓 = 𝑈 → ( 𝑍 ·s 𝑓 ) = ( 𝑍 ·s 𝑈 ) )
88	87	oveq1d	⊢ ( 𝑓 = 𝑈 → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑇 ) ) = ( ( 𝑍 ·s 𝑈 ) -s ( 𝑍 ·s 𝑇 ) ) )
89		oveq2	⊢ ( 𝑓 = 𝑈 → ( 𝑊 ·s 𝑓 ) = ( 𝑊 ·s 𝑈 ) )
90	89	oveq1d	⊢ ( 𝑓 = 𝑈 → ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑇 ) ) = ( ( 𝑊 ·s 𝑈 ) -s ( 𝑊 ·s 𝑇 ) ) )
91	88 90	breq12d	⊢ ( 𝑓 = 𝑈 → ( ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑇 ) ) ↔ ( ( 𝑍 ·s 𝑈 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑈 ) -s ( 𝑊 ·s 𝑇 ) ) ) )
92	86 91	imbi12d	⊢ ( 𝑓 = 𝑈 → ( ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑇 ) ) ) ↔ ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈 ) → ( ( 𝑍 ·s 𝑈 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑈 ) -s ( 𝑊 ·s 𝑇 ) ) ) ) )
93	92	anbi2d	⊢ ( 𝑓 = 𝑈 → ( ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑓 ) → ( ( 𝑍 ·s 𝑓 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑓 ) -s ( 𝑊 ·s 𝑇 ) ) ) ) ↔ ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈 ) → ( ( 𝑍 ·s 𝑈 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑈 ) -s ( 𝑊 ·s 𝑇 ) ) ) ) ) )
94	84 93	imbi12d	⊢ ( 𝑓 = 𝑈 → ( ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( 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 𝑇 ) ) ) ) ) ) )
95	16 24 41 58 76 94	rspc6v	⊢ ( ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) ∧ ( 𝑍 ∈ No ∧ 𝑊 ∈ No ) ∧ ( 𝑇 ∈ No ∧ 𝑈 ∈ No ) ) → ( ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( 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 𝑇 ) ) ) ) ) ) )
96	2 3 4 5 6 7 95	syl222anc	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 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 𝑒 ) ) ) ) ) → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 𝑍 ) +no ( bday ‘ 𝑇 ) ) ∪ ( ( 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 𝑇 ) ) ) ) ) ) )
97	1 8 96	mp2d	⊢ ( 𝜑 → ( ( 𝑋 ·s 𝑌 ) ∈ No ∧ ( ( 𝑍 <s 𝑊 ∧ 𝑇 <s 𝑈 ) → ( ( 𝑍 ·s 𝑈 ) -s ( 𝑍 ·s 𝑇 ) ) <s ( ( 𝑊 ·s 𝑈 ) -s ( 𝑊 ·s 𝑇 ) ) ) ) )