Theorem mulsproplemcbv 27811

Description: Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025.)

Hypothesis

Ref

Expression

mulsproplem.1

⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))

Assertion

Ref

Expression

mulsproplemcbv

⊢ (𝜑 → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐴,𝑔,ℎ,𝑖,𝑗,𝑘,𝑙,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑔,ℎ,𝑖,𝑗,𝑘,𝑙   𝐶,𝑔,ℎ,𝑖,𝑗,𝑘,𝑙   𝐷,𝑔,ℎ,𝑖,𝑗,𝑘,𝑙   𝑔,𝐸,ℎ,𝑖,𝑗,𝑘,𝑙   𝑔,𝐹,ℎ,𝑖,𝑗,𝑘,𝑙

Allowed substitution hints:   𝜑(𝑒,𝑓,𝑔,ℎ,𝑖,𝑗,𝑘,𝑎,𝑏,𝑐,𝑑,𝑙)

Proof of Theorem mulsproplemcbv

Step	Hyp	Ref	Expression
1		mulsproplem.1	. 2 ⊢ (𝜑 → ∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
2		fveq2 6891	. . . . . . 7 ⊢ (𝑎 = 𝑔 → ( bday ‘𝑎) = ( bday ‘𝑔))
3	2	oveq1d 7427	. . . . . 6 ⊢ (𝑎 = 𝑔 → (( bday ‘𝑎) +no ( bday ‘𝑏)) = (( bday ‘𝑔) +no ( bday ‘𝑏)))
4	3	uneq1d 4162	. . . . 5 ⊢ (𝑎 = 𝑔 → ((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) = ((( bday ‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))))
5	4	eleq1d 2817	. . . 4 ⊢ (𝑎 = 𝑔 → (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ↔ ((( bday ‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
6		oveq1 7419	. . . . . 6 ⊢ (𝑎 = 𝑔 → (𝑎 ·s 𝑏) = (𝑔 ·s 𝑏))
7	6	eleq1d 2817	. . . . 5 ⊢ (𝑎 = 𝑔 → ((𝑎 ·s 𝑏) ∈ No ↔ (𝑔 ·s 𝑏) ∈ No ))
8	7	anbi1d 629	. . . 4 ⊢ (𝑎 = 𝑔 → (((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
9	5, 8	imbi12d 344	. . 3 ⊢ (𝑎 = 𝑔 → ((((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ (((( bday ‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
10		fveq2 6891	. . . . . . 7 ⊢ (𝑏 = ℎ → ( bday ‘𝑏) = ( bday ‘ℎ))
11	10	oveq2d 7428	. . . . . 6 ⊢ (𝑏 = ℎ → (( bday ‘𝑔) +no ( bday ‘𝑏)) = (( bday ‘𝑔) +no ( bday ‘ℎ)))
12	11	uneq1d 4162	. . . . 5 ⊢ (𝑏 = ℎ → ((( bday ‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))))
13	12	eleq1d 2817	. . . 4 ⊢ (𝑏 = ℎ → (((( bday ‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ↔ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
14		oveq2 7420	. . . . . 6 ⊢ (𝑏 = ℎ → (𝑔 ·s 𝑏) = (𝑔 ·s ℎ))
15	14	eleq1d 2817	. . . . 5 ⊢ (𝑏 = ℎ → ((𝑔 ·s 𝑏) ∈ No ↔ (𝑔 ·s ℎ) ∈ No ))
16	15	anbi1d 629	. . . 4 ⊢ (𝑏 = ℎ → (((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
17	13, 16	imbi12d 344	. . 3 ⊢ (𝑏 = ℎ → ((((( bday ‘𝑔) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
18		fveq2 6891	. . . . . . . . 9 ⊢ (𝑐 = 𝑖 → ( bday ‘𝑐) = ( bday ‘𝑖))
19	18	oveq1d 7427	. . . . . . . 8 ⊢ (𝑐 = 𝑖 → (( bday ‘𝑐) +no ( bday ‘𝑒)) = (( bday ‘𝑖) +no ( bday ‘𝑒)))
20	19	uneq1d 4162	. . . . . . 7 ⊢ (𝑐 = 𝑖 → ((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))))
21	18	oveq1d 7427	. . . . . . . 8 ⊢ (𝑐 = 𝑖 → (( bday ‘𝑐) +no ( bday ‘𝑓)) = (( bday ‘𝑖) +no ( bday ‘𝑓)))
22	21	uneq1d 4162	. . . . . . 7 ⊢ (𝑐 = 𝑖 → ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))
23	20, 22	uneq12d 4164	. . . . . 6 ⊢ (𝑐 = 𝑖 → (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒)))) = (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒)))))
24	23	uneq2d 4163	. . . . 5 ⊢ (𝑐 = 𝑖 → ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))))
25	24	eleq1d 2817	. . . 4 ⊢ (𝑐 = 𝑖 → (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ↔ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
26		breq1 5151	. . . . . . 7 ⊢ (𝑐 = 𝑖 → (𝑐 <s 𝑑 ↔ 𝑖 <s 𝑑))
27	26	anbi1d 629	. . . . . 6 ⊢ (𝑐 = 𝑖 → ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓)))
28		oveq1 7419	. . . . . . . 8 ⊢ (𝑐 = 𝑖 → (𝑐 ·s 𝑓) = (𝑖 ·s 𝑓))
29		oveq1 7419	. . . . . . . 8 ⊢ (𝑐 = 𝑖 → (𝑐 ·s 𝑒) = (𝑖 ·s 𝑒))
30	28, 29	oveq12d 7430	. . . . . . 7 ⊢ (𝑐 = 𝑖 → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)))
31	30	breq1d 5158	. . . . . 6 ⊢ (𝑐 = 𝑖 → (((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))
32	27, 31	imbi12d 344	. . . . 5 ⊢ (𝑐 = 𝑖 → (((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))
33	32	anbi2d 628	. . . 4 ⊢ (𝑐 = 𝑖 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))))
34	25, 33	imbi12d 344	. . 3 ⊢ (𝑐 = 𝑖 → ((((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))))
35		fveq2 6891	. . . . . . . . 9 ⊢ (𝑑 = 𝑗 → ( bday ‘𝑑) = ( bday ‘𝑗))
36	35	oveq1d 7427	. . . . . . . 8 ⊢ (𝑑 = 𝑗 → (( bday ‘𝑑) +no ( bday ‘𝑓)) = (( bday ‘𝑗) +no ( bday ‘𝑓)))
37	36	uneq2d 4163	. . . . . . 7 ⊢ (𝑑 = 𝑗 → ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))))
38	35	oveq1d 7427	. . . . . . . 8 ⊢ (𝑑 = 𝑗 → (( bday ‘𝑑) +no ( bday ‘𝑒)) = (( bday ‘𝑗) +no ( bday ‘𝑒)))
39	38	uneq2d 4163	. . . . . . 7 ⊢ (𝑑 = 𝑗 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))
40	37, 39	uneq12d 4164	. . . . . 6 ⊢ (𝑑 = 𝑗 → (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒)))) = (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒)))))
41	40	uneq2d 4163	. . . . 5 ⊢ (𝑑 = 𝑗 → ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))))
42	41	eleq1d 2817	. . . 4 ⊢ (𝑑 = 𝑗 → (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ↔ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
43		breq2 5152	. . . . . . 7 ⊢ (𝑑 = 𝑗 → (𝑖 <s 𝑑 ↔ 𝑖 <s 𝑗))
44	43	anbi1d 629	. . . . . 6 ⊢ (𝑑 = 𝑗 → ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓)))
45		oveq1 7419	. . . . . . . 8 ⊢ (𝑑 = 𝑗 → (𝑑 ·s 𝑓) = (𝑗 ·s 𝑓))
46		oveq1 7419	. . . . . . . 8 ⊢ (𝑑 = 𝑗 → (𝑑 ·s 𝑒) = (𝑗 ·s 𝑒))
47	45, 46	oveq12d 7430	. . . . . . 7 ⊢ (𝑑 = 𝑗 → ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))
48	47	breq2d 5160	. . . . . 6 ⊢ (𝑑 = 𝑗 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))
49	44, 48	imbi12d 344	. . . . 5 ⊢ (𝑑 = 𝑗 → (((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))) ↔ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))))
50	49	anbi2d 628	. . . 4 ⊢ (𝑑 = 𝑗 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))))
51	42, 50	imbi12d 344	. . 3 ⊢ (𝑑 = 𝑗 → ((((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))))))
52		fveq2 6891	. . . . . . . . 9 ⊢ (𝑒 = 𝑘 → ( bday ‘𝑒) = ( bday ‘𝑘))
53	52	oveq2d 7428	. . . . . . . 8 ⊢ (𝑒 = 𝑘 → (( bday ‘𝑖) +no ( bday ‘𝑒)) = (( bday ‘𝑖) +no ( bday ‘𝑘)))
54	53	uneq1d 4162	. . . . . . 7 ⊢ (𝑒 = 𝑘 → ((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))))
55	52	oveq2d 7428	. . . . . . . 8 ⊢ (𝑒 = 𝑘 → (( bday ‘𝑗) +no ( bday ‘𝑒)) = (( bday ‘𝑗) +no ( bday ‘𝑘)))
56	55	uneq2d 4163	. . . . . . 7 ⊢ (𝑒 = 𝑘 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))) = ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))
57	54, 56	uneq12d 4164	. . . . . 6 ⊢ (𝑒 = 𝑘 → (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒)))) = (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))
58	57	uneq2d 4163	. . . . 5 ⊢ (𝑒 = 𝑘 → ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))) = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))))
59	58	eleq1d 2817	. . . 4 ⊢ (𝑒 = 𝑘 → (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ↔ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
60		breq1 5151	. . . . . . 7 ⊢ (𝑒 = 𝑘 → (𝑒 <s 𝑓 ↔ 𝑘 <s 𝑓))
61	60	anbi2d 628	. . . . . 6 ⊢ (𝑒 = 𝑘 → ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓)))
62		oveq2 7420	. . . . . . . 8 ⊢ (𝑒 = 𝑘 → (𝑖 ·s 𝑒) = (𝑖 ·s 𝑘))
63	62	oveq2d 7428	. . . . . . 7 ⊢ (𝑒 = 𝑘 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) = ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)))
64		oveq2 7420	. . . . . . . 8 ⊢ (𝑒 = 𝑘 → (𝑗 ·s 𝑒) = (𝑗 ·s 𝑘))
65	64	oveq2d 7428	. . . . . . 7 ⊢ (𝑒 = 𝑘 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) = ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))
66	63, 65	breq12d 5161	. . . . . 6 ⊢ (𝑒 = 𝑘 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)) ↔ ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))
67	61, 66	imbi12d 344	. . . . 5 ⊢ (𝑒 = 𝑘 → (((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))) ↔ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))))
68	67	anbi2d 628	. . . 4 ⊢ (𝑒 = 𝑘 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))))
69	59, 68	imbi12d 344	. . 3 ⊢ (𝑒 = 𝑘 → ((((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑒)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑒))))) ↔ (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))))))
70		fveq2 6891	. . . . . . . . 9 ⊢ (𝑓 = 𝑙 → ( bday ‘𝑓) = ( bday ‘𝑙))
71	70	oveq2d 7428	. . . . . . . 8 ⊢ (𝑓 = 𝑙 → (( bday ‘𝑗) +no ( bday ‘𝑓)) = (( bday ‘𝑗) +no ( bday ‘𝑙)))
72	71	uneq2d 4163	. . . . . . 7 ⊢ (𝑓 = 𝑙 → ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) = ((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))))
73	70	oveq2d 7428	. . . . . . . 8 ⊢ (𝑓 = 𝑙 → (( bday ‘𝑖) +no ( bday ‘𝑓)) = (( bday ‘𝑖) +no ( bday ‘𝑙)))
74	73	uneq1d 4162	. . . . . . 7 ⊢ (𝑓 = 𝑙 → ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))) = ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))
75	72, 74	uneq12d 4164	. . . . . 6 ⊢ (𝑓 = 𝑙 → (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))) = (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘)))))
76	75	uneq2d 4163	. . . . 5 ⊢ (𝑓 = 𝑙 → ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) = ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))))
77	76	eleq1d 2817	. . . 4 ⊢ (𝑓 = 𝑙 → (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) ↔ ((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸)))))))
78		breq2 5152	. . . . . . 7 ⊢ (𝑓 = 𝑙 → (𝑘 <s 𝑓 ↔ 𝑘 <s 𝑙))
79	78	anbi2d 628	. . . . . 6 ⊢ (𝑓 = 𝑙 → ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) ↔ (𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙)))
80		oveq2 7420	. . . . . . . 8 ⊢ (𝑓 = 𝑙 → (𝑖 ·s 𝑓) = (𝑖 ·s 𝑙))
81	80	oveq1d 7427	. . . . . . 7 ⊢ (𝑓 = 𝑙 → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) = ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)))
82		oveq2 7420	. . . . . . . 8 ⊢ (𝑓 = 𝑙 → (𝑗 ·s 𝑓) = (𝑗 ·s 𝑙))
83	82	oveq1d 7427	. . . . . . 7 ⊢ (𝑓 = 𝑙 → ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) = ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))
84	81, 83	breq12d 5161	. . . . . 6 ⊢ (𝑓 = 𝑙 → (((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)) ↔ ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))
85	79, 84	imbi12d 344	. . . . 5 ⊢ (𝑓 = 𝑙 → (((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))) ↔ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))
86	85	anbi2d 628	. . . 4 ⊢ (𝑓 = 𝑙 → (((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘)))) ↔ ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
87	77, 86	imbi12d 344	. . 3 ⊢ (𝑓 = 𝑙 → ((((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓) → ((𝑖 ·s 𝑓) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑓) -s (𝑗 ·s 𝑘))))) ↔ (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘)))))))
88	9, 17, 34, 51, 69, 87	cbvral6vw 3241	. 2 ⊢ (∀𝑎 ∈ No ∀𝑏 ∈ No ∀𝑐 ∈ No ∀𝑑 ∈ No ∀𝑒 ∈ No ∀𝑓 ∈ No (((( bday ‘𝑎) +no ( bday ‘𝑏)) ∪ (((( bday ‘𝑐) +no ( bday ‘𝑒)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑓))) ∪ ((( bday ‘𝑐) +no ( bday ‘𝑓)) ∪ (( bday ‘𝑑) +no ( bday ‘𝑒))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑎 ·s 𝑏) ∈ No ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒))))) ↔ ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))
89	1, 88	sylib 217	1 ⊢ (𝜑 → ∀𝑔 ∈ No ∀ℎ ∈ No ∀𝑖 ∈ No ∀𝑗 ∈ No ∀𝑘 ∈ No ∀𝑙 ∈ No (((( bday ‘𝑔) +no ( bday ‘ℎ)) ∪ (((( bday ‘𝑖) +no ( bday ‘𝑘)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑙))) ∪ ((( bday ‘𝑖) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑗) +no ( bday ‘𝑘))))) ∈ ((( bday ‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday ‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday ‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday ‘𝐷) +no ( bday ‘𝐸))))) → ((𝑔 ·s ℎ) ∈ No ∧ ((𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙) → ((𝑖 ·s 𝑙) -s (𝑖 ·s 𝑘)) <s ((𝑗 ·s 𝑙) -s (𝑗 ·s 𝑘))))))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3060   ∪ cun 3946   class class class wbr 5148  ‘cfv 6543  (class class class)co 7412   +no cnadd 8668   No csur 27380   <s cslt 27381   bday cbday 27382   -_s csubs 27735   ·_s cmuls 27802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415

This theorem is referenced by:  mulsproplem13  27824  mulsproplem14  27825