Theorem mulsprop

Description: Surreals are closed under multiplication and obey a particular ordering law. Theorem 3.4 of Gonshor p. 17. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Assertion	mulsprop	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ ( 𝐸 ∈ No ∧ 𝐹 ∈ No ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
2		bdayelon	⊢ ( bday ‘ 𝐵 ) ∈ On
3		naddcl	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On )
4	1 2 3	mp2an	⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On
5		bdayelon	⊢ ( bday ‘ 𝐶 ) ∈ On
6		bdayelon	⊢ ( bday ‘ 𝐸 ) ∈ On
7		naddcl	⊢ ( ( ( bday ‘ 𝐶 ) ∈ On ∧ ( bday ‘ 𝐸 ) ∈ On ) → ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∈ On )
8	5 6 7	mp2an	⊢ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∈ On
9		bdayelon	⊢ ( bday ‘ 𝐷 ) ∈ On
10		bdayelon	⊢ ( bday ‘ 𝐹 ) ∈ On
11		naddcl	⊢ ( ( ( bday ‘ 𝐷 ) ∈ On ∧ ( bday ‘ 𝐹 ) ∈ On ) → ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ∈ On )
12	9 10 11	mp2an	⊢ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ∈ On
13	8 12	onun2i	⊢ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∈ On
14		naddcl	⊢ ( ( ( bday ‘ 𝐶 ) ∈ On ∧ ( bday ‘ 𝐹 ) ∈ On ) → ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∈ On )
15	5 10 14	mp2an	⊢ ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∈ On
16		naddcl	⊢ ( ( ( bday ‘ 𝐷 ) ∈ On ∧ ( bday ‘ 𝐸 ) ∈ On ) → ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ∈ On )
17	9 6 16	mp2an	⊢ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ∈ On
18	15 17	onun2i	⊢ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ∈ On
19	13 18	onun2i	⊢ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ∈ On
20	4 19	onun2i	⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ∈ On
21		risset	⊢ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ∈ On ↔ ∃ 𝑥 ∈ On 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
22	20 21	mpbi	⊢ ∃ 𝑥 ∈ On 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) )
23		fveq2	⊢ ( 𝑎 = 𝑔 → ( bday ‘ 𝑎 ) = ( bday ‘ 𝑔 ) )
24	23	oveq1d	⊢ ( 𝑎 = 𝑔 → ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) = ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑏 ) ) )
25	24	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 ‘ 𝑒 ) ) ) ) ) )
26	25	eqeq2d	⊢ ( 𝑎 = 𝑔 → ( 𝑥 = ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ) )
27		oveq1	⊢ ( 𝑎 = 𝑔 → ( 𝑎 ·s 𝑏 ) = ( 𝑔 ·s 𝑏 ) )
28	27	eleq1d	⊢ ( 𝑎 = 𝑔 → ( ( 𝑎 ·s 𝑏 ) ∈ No ↔ ( 𝑔 ·s 𝑏 ) ∈ No ) )
29	28	anbi1d	⊢ ( 𝑎 = 𝑔 → ( ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑔 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
30	26 29	imbi12d	⊢ ( 𝑎 = 𝑔 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑒 ) ) ) ) ) → ( ( 𝑔 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) ) )
31		fveq2	⊢ ( 𝑏 = ℎ → ( bday ‘ 𝑏 ) = ( bday ‘ ℎ ) )
32	31	oveq2d	⊢ ( 𝑏 = ℎ → ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑏 ) ) = ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) )
33	32	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 ‘ 𝑒 ) ) ) ) ) )
34	33	eqeq2d	⊢ ( 𝑏 = ℎ → ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ) )
35		oveq2	⊢ ( 𝑏 = ℎ → ( 𝑔 ·s 𝑏 ) = ( 𝑔 ·s ℎ ) )
36	35	eleq1d	⊢ ( 𝑏 = ℎ → ( ( 𝑔 ·s 𝑏 ) ∈ No ↔ ( 𝑔 ·s ℎ ) ∈ No ) )
37	36	anbi1d	⊢ ( 𝑏 = ℎ → ( ( ( 𝑔 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
38	34 37	imbi12d	⊢ ( 𝑏 = ℎ → ( ( 𝑥 = ( ( ( 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 ‘ 𝑒 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) ) )
39		fveq2	⊢ ( 𝑐 = 𝑖 → ( bday ‘ 𝑐 ) = ( bday ‘ 𝑖 ) )
40	39	oveq1d	⊢ ( 𝑐 = 𝑖 → ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) = ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) )
41	40	uneq1d	⊢ ( 𝑐 = 𝑖 → ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) = ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) )
42	39	oveq1d	⊢ ( 𝑐 = 𝑖 → ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) = ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) )
43	42	uneq1d	⊢ ( 𝑐 = 𝑖 → ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) = ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) )
44	41 43	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 ‘ 𝑒 ) ) ) ) )
45	44	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 ‘ 𝑒 ) ) ) ) ) )
46	45	eqeq2d	⊢ ( 𝑐 = 𝑖 → ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ) )
47		breq1	⊢ ( 𝑐 = 𝑖 → ( 𝑐 <s 𝑑 ↔ 𝑖 <s 𝑑 ) )
48	47	anbi1d	⊢ ( 𝑐 = 𝑖 → ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) ↔ ( 𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓 ) ) )
49		oveq1	⊢ ( 𝑐 = 𝑖 → ( 𝑐 ·s 𝑓 ) = ( 𝑖 ·s 𝑓 ) )
50		oveq1	⊢ ( 𝑐 = 𝑖 → ( 𝑐 ·s 𝑒 ) = ( 𝑖 ·s 𝑒 ) )
51	49 50	oveq12d	⊢ ( 𝑐 = 𝑖 → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) = ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) )
52	51	breq1d	⊢ ( 𝑐 = 𝑖 → ( ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ↔ ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) )
53	48 52	imbi12d	⊢ ( 𝑐 = 𝑖 → ( ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ↔ ( ( 𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) )
54	53	anbi2d	⊢ ( 𝑐 = 𝑖 → ( ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
55	46 54	imbi12d	⊢ ( 𝑐 = 𝑖 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑒 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) ) )
56		fveq2	⊢ ( 𝑑 = 𝑗 → ( bday ‘ 𝑑 ) = ( bday ‘ 𝑗 ) )
57	56	oveq1d	⊢ ( 𝑑 = 𝑗 → ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) = ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) )
58	57	uneq2d	⊢ ( 𝑑 = 𝑗 → ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) = ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) ) )
59	56	oveq1d	⊢ ( 𝑑 = 𝑗 → ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) = ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑒 ) ) )
60	59	uneq2d	⊢ ( 𝑑 = 𝑗 → ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) = ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑒 ) ) ) )
61	58 60	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 ‘ 𝑒 ) ) ) ) )
62	61	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 ‘ 𝑒 ) ) ) ) ) )
63	62	eqeq2d	⊢ ( 𝑑 = 𝑗 → ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ) )
64		breq2	⊢ ( 𝑑 = 𝑗 → ( 𝑖 <s 𝑑 ↔ 𝑖 <s 𝑗 ) )
65	64	anbi1d	⊢ ( 𝑑 = 𝑗 → ( ( 𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓 ) ↔ ( 𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓 ) ) )
66		oveq1	⊢ ( 𝑑 = 𝑗 → ( 𝑑 ·s 𝑓 ) = ( 𝑗 ·s 𝑓 ) )
67		oveq1	⊢ ( 𝑑 = 𝑗 → ( 𝑑 ·s 𝑒 ) = ( 𝑗 ·s 𝑒 ) )
68	66 67	oveq12d	⊢ ( 𝑑 = 𝑗 → ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) = ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) )
69	68	breq2d	⊢ ( 𝑑 = 𝑗 → ( ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ↔ ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) )
70	65 69	imbi12d	⊢ ( 𝑑 = 𝑗 → ( ( ( 𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ↔ ( ( 𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) ) )
71	70	anbi2d	⊢ ( 𝑑 = 𝑗 → ( ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) ) ) )
72	63 71	imbi12d	⊢ ( 𝑑 = 𝑗 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑒 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) ) ) ) )
73		fveq2	⊢ ( 𝑒 = 𝑘 → ( bday ‘ 𝑒 ) = ( bday ‘ 𝑘 ) )
74	73	oveq2d	⊢ ( 𝑒 = 𝑘 → ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) = ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) )
75	74	uneq1d	⊢ ( 𝑒 = 𝑘 → ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) ) = ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) ) )
76	73	oveq2d	⊢ ( 𝑒 = 𝑘 → ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑒 ) ) = ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) )
77	76	uneq2d	⊢ ( 𝑒 = 𝑘 → ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑒 ) ) ) = ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) )
78	75 77	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 ‘ 𝑘 ) ) ) ) )
79	78	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 ‘ 𝑘 ) ) ) ) ) )
80	79	eqeq2d	⊢ ( 𝑒 = 𝑘 → ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ) )
81		breq1	⊢ ( 𝑒 = 𝑘 → ( 𝑒 <s 𝑓 ↔ 𝑘 <s 𝑓 ) )
82	81	anbi2d	⊢ ( 𝑒 = 𝑘 → ( ( 𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓 ) ↔ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓 ) ) )
83		oveq2	⊢ ( 𝑒 = 𝑘 → ( 𝑖 ·s 𝑒 ) = ( 𝑖 ·s 𝑘 ) )
84	83	oveq2d	⊢ ( 𝑒 = 𝑘 → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) = ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) )
85		oveq2	⊢ ( 𝑒 = 𝑘 → ( 𝑗 ·s 𝑒 ) = ( 𝑗 ·s 𝑘 ) )
86	85	oveq2d	⊢ ( 𝑒 = 𝑘 → ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) = ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) )
87	84 86	breq12d	⊢ ( 𝑒 = 𝑘 → ( ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ↔ ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) )
88	82 87	imbi12d	⊢ ( 𝑒 = 𝑘 → ( ( ( 𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) ↔ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) )
89	88	anbi2d	⊢ ( 𝑒 = 𝑘 → ( ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) ) ↔ ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
90	80 89	imbi12d	⊢ ( 𝑒 = 𝑘 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) ) )
91		fveq2	⊢ ( 𝑓 = 𝑙 → ( bday ‘ 𝑓 ) = ( bday ‘ 𝑙 ) )
92	91	oveq2d	⊢ ( 𝑓 = 𝑙 → ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) = ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) )
93	92	uneq2d	⊢ ( 𝑓 = 𝑙 → ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) ) = ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) )
94	91	oveq2d	⊢ ( 𝑓 = 𝑙 → ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) = ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) )
95	94	uneq1d	⊢ ( 𝑓 = 𝑙 → ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) = ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) )
96	93 95	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 ‘ 𝑘 ) ) ) ) )
97	96	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 ‘ 𝑘 ) ) ) ) ) )
98	97	eqeq2d	⊢ ( 𝑓 = 𝑙 → ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ) )
99		breq2	⊢ ( 𝑓 = 𝑙 → ( 𝑘 <s 𝑓 ↔ 𝑘 <s 𝑙 ) )
100	99	anbi2d	⊢ ( 𝑓 = 𝑙 → ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓 ) ↔ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) )
101		oveq2	⊢ ( 𝑓 = 𝑙 → ( 𝑖 ·s 𝑓 ) = ( 𝑖 ·s 𝑙 ) )
102	101	oveq1d	⊢ ( 𝑓 = 𝑙 → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) = ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) )
103		oveq2	⊢ ( 𝑓 = 𝑙 → ( 𝑗 ·s 𝑓 ) = ( 𝑗 ·s 𝑙 ) )
104	103	oveq1d	⊢ ( 𝑓 = 𝑙 → ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) = ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) )
105	102 104	breq12d	⊢ ( 𝑓 = 𝑙 → ( ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ↔ ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) )
106	100 105	imbi12d	⊢ ( 𝑓 = 𝑙 → ( ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) ↔ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) )
107	106	anbi2d	⊢ ( 𝑓 = 𝑙 → ( ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ↔ ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
108	98 107	imbi12d	⊢ ( 𝑓 = 𝑙 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) ) )
109	30 38 55 72 90 108	cbvral6vw	⊢ ( ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑥 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
110		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ↔ 𝑦 = ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ) )
111	110	imbi1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑒 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) ) )
112	111	6ralbidv	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑥 = ( ( ( 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 ‘ 𝑒 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) ) )
113	109 112	bitr3id	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑔 ∈ No ∀ ℎ ∈ No ∀ 𝑖 ∈ No ∀ 𝑗 ∈ No ∀ 𝑘 ∈ No ∀ 𝑙 ∈ No ( 𝑥 = ( ( ( 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 ‘ 𝑒 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) ) )
114		raleq	⊢ ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) → ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 𝑒 ) ) ) ) ) ) )
115		ralrot3	⊢ ( ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 𝑒 ) ) ) ) ) )
116		ralrot3	⊢ ( ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 𝑒 ) ) ) ) ) )
117		ralrot3	⊢ ( ∀ 𝑒 ∈ 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 ‘ 𝑘 ) ) ) ) ) ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 𝑒 ) ) ) ) ) )
118		r19.23v	⊢ ( ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
119		risset	⊢ ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ↔ ∃ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) 𝑦 = ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) )
120	119	imbi1i	⊢ ( ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
121	118 120	bitr4i	⊢ ( ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
122	121	2ralbii	⊢ ( ∀ 𝑒 ∈ 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 ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
123	117 122	bitr3i	⊢ ( ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
124	123	2ralbii	⊢ ( ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
125	116 124	bitr3i	⊢ ( ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( 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 𝑒 ) ) ) ) ) )
126	125	2ralbii	⊢ ( ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 𝑒 ) ) ) ) ) )
127	115 126	bitr3i	⊢ ( ∀ 𝑦 ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) ↔ ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
128	114 127	bitrdi	⊢ ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) → ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 𝑒 ) ) ) ) ) ) )
129		simpl	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → ∀ 𝑎 ∈ 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		simprl1	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → 𝑔 ∈ No )
131		simprl2	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → ℎ ∈ No )
132	129 130 131	mulsproplem11	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → ( 𝑔 ·s ℎ ) ∈ No )
133	129	adantr	⊢ ( ( ( ∀ 𝑎 ∈ 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 ) ) ) ∧ ( 𝑖 <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 𝑒 ) ) ) ) ) )
134		simprl3	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → 𝑖 ∈ No )
135	134	adantr	⊢ ( ( ( ∀ 𝑎 ∈ 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 ) ) ) ∧ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) → 𝑖 ∈ No )
136		simprr1	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → 𝑗 ∈ No )
137	136	adantr	⊢ ( ( ( ∀ 𝑎 ∈ 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 ) ) ) ∧ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) → 𝑗 ∈ No )
138		simprr2	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → 𝑘 ∈ No )
139	138	adantr	⊢ ( ( ( ∀ 𝑎 ∈ 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 ) ) ) ∧ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) → 𝑘 ∈ No )
140		simprr3	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → 𝑙 ∈ No )
141	140	adantr	⊢ ( ( ( ∀ 𝑎 ∈ 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 ) ) ) ∧ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) → 𝑙 ∈ No )
142		simprl	⊢ ( ( ( ∀ 𝑎 ∈ 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 ) ) ) ∧ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) → 𝑖 <s 𝑗 )
143		simprr	⊢ ( ( ( ∀ 𝑎 ∈ 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 ) ) ) ∧ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) → 𝑘 <s 𝑙 )
144	133 135 137 139 141 142 143	mulsproplem14	⊢ ( ( ( ∀ 𝑎 ∈ 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 ) ) ) ∧ ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) )
145	144	ex	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) )
146	132 145	jca	⊢ ( ( ∀ 𝑎 ∈ 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 ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) )
147	146	ex	⊢ ( ∀ 𝑎 ∈ 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 ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
148	128 147	biimtrdi	⊢ ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) → ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) ) )
149	148	impd	⊢ ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) → ( ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
150	149	com12	⊢ ( ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
151	150	anassrs	⊢ ( ( ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
152	151	ralrimivvva	⊢ ( ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
153	152	ralrimivvva	⊢ ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
154	153	a1i	⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( 𝑦 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) ) )
155	113 154	tfis2	⊢ ( 𝑥 ∈ On → ∀ 𝑔 ∈ No ∀ ℎ ∈ No ∀ 𝑖 ∈ No ∀ 𝑗 ∈ No ∀ 𝑘 ∈ No ∀ 𝑙 ∈ No ( 𝑥 = ( ( ( 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		fveq2	⊢ ( 𝑔 = 𝐴 → ( bday ‘ 𝑔 ) = ( bday ‘ 𝐴 ) )
157	156	oveq1d	⊢ ( 𝑔 = 𝐴 → ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ ℎ ) ) )
158	157	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 ‘ 𝑘 ) ) ) ) ) )
159	158	eqeq2d	⊢ ( 𝑔 = 𝐴 → ( 𝑥 = ( ( ( bday ‘ 𝑔 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ) )
160		oveq1	⊢ ( 𝑔 = 𝐴 → ( 𝑔 ·s ℎ ) = ( 𝐴 ·s ℎ ) )
161	160	eleq1d	⊢ ( 𝑔 = 𝐴 → ( ( 𝑔 ·s ℎ ) ∈ No ↔ ( 𝐴 ·s ℎ ) ∈ No ) )
162	161	anbi1d	⊢ ( 𝑔 = 𝐴 → ( ( ( 𝑔 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ↔ ( ( 𝐴 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
163	159 162	imbi12d	⊢ ( 𝑔 = 𝐴 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝐴 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) ) )
164		fveq2	⊢ ( ℎ = 𝐵 → ( bday ‘ ℎ ) = ( bday ‘ 𝐵 ) )
165	164	oveq2d	⊢ ( ℎ = 𝐵 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ ℎ ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
166	165	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 ‘ 𝑘 ) ) ) ) ) )
167	166	eqeq2d	⊢ ( ℎ = 𝐵 → ( 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ ℎ ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ) )
168		oveq2	⊢ ( ℎ = 𝐵 → ( 𝐴 ·s ℎ ) = ( 𝐴 ·s 𝐵 ) )
169	168	eleq1d	⊢ ( ℎ = 𝐵 → ( ( 𝐴 ·s ℎ ) ∈ No ↔ ( 𝐴 ·s 𝐵 ) ∈ No ) )
170	169	anbi1d	⊢ ( ℎ = 𝐵 → ( ( ( 𝐴 ·s ℎ ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ↔ ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
171	167 170	imbi12d	⊢ ( ℎ = 𝐵 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) ) )
172		fveq2	⊢ ( 𝑖 = 𝐶 → ( bday ‘ 𝑖 ) = ( bday ‘ 𝐶 ) )
173	172	oveq1d	⊢ ( 𝑖 = 𝐶 → ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) = ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) )
174	173	uneq1d	⊢ ( 𝑖 = 𝐶 → ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) = ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) )
175	172	oveq1d	⊢ ( 𝑖 = 𝐶 → ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) )
176	175	uneq1d	⊢ ( 𝑖 = 𝐶 → ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) = ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) )
177	174 176	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 ‘ 𝑘 ) ) ) ) )
178	177	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 ‘ 𝑘 ) ) ) ) ) )
179	178	eqeq2d	⊢ ( 𝑖 = 𝐶 → ( 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝑖 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ) )
180		breq1	⊢ ( 𝑖 = 𝐶 → ( 𝑖 <s 𝑗 ↔ 𝐶 <s 𝑗 ) )
181	180	anbi1d	⊢ ( 𝑖 = 𝐶 → ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ↔ ( 𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ) )
182		oveq1	⊢ ( 𝑖 = 𝐶 → ( 𝑖 ·s 𝑙 ) = ( 𝐶 ·s 𝑙 ) )
183		oveq1	⊢ ( 𝑖 = 𝐶 → ( 𝑖 ·s 𝑘 ) = ( 𝐶 ·s 𝑘 ) )
184	182 183	oveq12d	⊢ ( 𝑖 = 𝐶 → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) = ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) )
185	184	breq1d	⊢ ( 𝑖 = 𝐶 → ( ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ↔ ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) )
186	181 185	imbi12d	⊢ ( 𝑖 = 𝐶 → ( ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ↔ ( ( 𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) )
187	186	anbi2d	⊢ ( 𝑖 = 𝐶 → ( ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝑖 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ↔ ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) )
188	179 187	imbi12d	⊢ ( 𝑖 = 𝐶 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ) ) )
189		fveq2	⊢ ( 𝑗 = 𝐷 → ( bday ‘ 𝑗 ) = ( bday ‘ 𝐷 ) )
190	189	oveq1d	⊢ ( 𝑗 = 𝐷 → ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) )
191	190	uneq2d	⊢ ( 𝑗 = 𝐷 → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) = ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) ) )
192	189	oveq1d	⊢ ( 𝑗 = 𝐷 → ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) = ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑘 ) ) )
193	192	uneq2d	⊢ ( 𝑗 = 𝐷 → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) = ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑘 ) ) ) )
194	191 193	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 ‘ 𝑘 ) ) ) ) )
195	194	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 ‘ 𝑘 ) ) ) ) ) )
196	195	eqeq2d	⊢ ( 𝑗 = 𝐷 → ( 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑗 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ) )
197		breq2	⊢ ( 𝑗 = 𝐷 → ( 𝐶 <s 𝑗 ↔ 𝐶 <s 𝐷 ) )
198	197	anbi1d	⊢ ( 𝑗 = 𝐷 → ( ( 𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙 ) ↔ ( 𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙 ) ) )
199		oveq1	⊢ ( 𝑗 = 𝐷 → ( 𝑗 ·s 𝑙 ) = ( 𝐷 ·s 𝑙 ) )
200		oveq1	⊢ ( 𝑗 = 𝐷 → ( 𝑗 ·s 𝑘 ) = ( 𝐷 ·s 𝑘 ) )
201	199 200	oveq12d	⊢ ( 𝑗 = 𝐷 → ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) = ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) )
202	201	breq2d	⊢ ( 𝑗 = 𝐷 → ( ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ↔ ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) ) )
203	198 202	imbi12d	⊢ ( 𝑗 = 𝐷 → ( ( ( 𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ↔ ( ( 𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) ) ) )
204	203	anbi2d	⊢ ( 𝑗 = 𝐷 → ( ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝑗 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) ↔ ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) ) ) ) )
205	196 204	imbi12d	⊢ ( 𝑗 = 𝐷 → ( ( 𝑥 = ( ( ( 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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) ) ) ) ) )
206		fveq2	⊢ ( 𝑘 = 𝐸 → ( bday ‘ 𝑘 ) = ( bday ‘ 𝐸 ) )
207	206	oveq2d	⊢ ( 𝑘 = 𝐸 → ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) = ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) )
208	207	uneq1d	⊢ ( 𝑘 = 𝐸 → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) ) = ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) ) )
209	206	oveq2d	⊢ ( 𝑘 = 𝐸 → ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑘 ) ) = ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) )
210	209	uneq2d	⊢ ( 𝑘 = 𝐸 → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑘 ) ) ) = ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
211	208 210	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 ‘ 𝐸 ) ) ) ) )
212	211	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 ‘ 𝐸 ) ) ) ) ) )
213	212	eqeq2d	⊢ ( 𝑘 = 𝐸 → ( 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑘 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑘 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ) )
214		breq1	⊢ ( 𝑘 = 𝐸 → ( 𝑘 <s 𝑙 ↔ 𝐸 <s 𝑙 ) )
215	214	anbi2d	⊢ ( 𝑘 = 𝐸 → ( ( 𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙 ) ↔ ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙 ) ) )
216		oveq2	⊢ ( 𝑘 = 𝐸 → ( 𝐶 ·s 𝑘 ) = ( 𝐶 ·s 𝐸 ) )
217	216	oveq2d	⊢ ( 𝑘 = 𝐸 → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) = ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) )
218		oveq2	⊢ ( 𝑘 = 𝐸 → ( 𝐷 ·s 𝑘 ) = ( 𝐷 ·s 𝐸 ) )
219	218	oveq2d	⊢ ( 𝑘 = 𝐸 → ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) = ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) )
220	217 219	breq12d	⊢ ( 𝑘 = 𝐸 → ( ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) ↔ ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) ) )
221	215 220	imbi12d	⊢ ( 𝑘 = 𝐸 → ( ( ( 𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) ) ↔ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) )
222	221	anbi2d	⊢ ( 𝑘 = 𝐸 → ( ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝑘 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝑘 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝑘 ) ) ) ) ↔ ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) ) )
223	213 222	imbi12d	⊢ ( 𝑘 = 𝐸 → ( ( 𝑥 = ( ( ( 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 ‘ 𝐸 ) ) ) ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) ) ) )
224		fveq2	⊢ ( 𝑙 = 𝐹 → ( bday ‘ 𝑙 ) = ( bday ‘ 𝐹 ) )
225	224	oveq2d	⊢ ( 𝑙 = 𝐹 → ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) )
226	225	uneq2d	⊢ ( 𝑙 = 𝐹 → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) ) = ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) )
227	224	oveq2d	⊢ ( 𝑙 = 𝐹 → ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) )
228	227	uneq1d	⊢ ( 𝑙 = 𝐹 → ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) = ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) )
229	226 228	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 ‘ 𝐸 ) ) ) ) )
230	229	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 ‘ 𝐸 ) ) ) ) ) )
231	230	eqeq2d	⊢ ( 𝑙 = 𝐹 → ( 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝑙 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ↔ 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) ) )
232		breq2	⊢ ( 𝑙 = 𝐹 → ( 𝐸 <s 𝑙 ↔ 𝐸 <s 𝐹 ) )
233	232	anbi2d	⊢ ( 𝑙 = 𝐹 → ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙 ) ↔ ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) ) )
234		oveq2	⊢ ( 𝑙 = 𝐹 → ( 𝐶 ·s 𝑙 ) = ( 𝐶 ·s 𝐹 ) )
235	234	oveq1d	⊢ ( 𝑙 = 𝐹 → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) = ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) )
236		oveq2	⊢ ( 𝑙 = 𝐹 → ( 𝐷 ·s 𝑙 ) = ( 𝐷 ·s 𝐹 ) )
237	236	oveq1d	⊢ ( 𝑙 = 𝐹 → ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) = ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) )
238	235 237	breq12d	⊢ ( 𝑙 = 𝐹 → ( ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) ↔ ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) )
239	233 238	imbi12d	⊢ ( 𝑙 = 𝐹 → ( ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) ) ↔ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) )
240	239	anbi2d	⊢ ( 𝑙 = 𝐹 → ( ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝑙 ) → ( ( 𝐶 ·s 𝑙 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝑙 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) ↔ ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) ) )
241	231 240	imbi12d	⊢ ( 𝑙 = 𝐹 → ( ( 𝑥 = ( ( ( 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 ‘ 𝐸 ) ) ) ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) ) ) )
242	163 171 188 205 223 241	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 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑔 ·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 ‘ 𝐸 ) ) ) ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) ) ) )
243	155 242	syl5com	⊢ ( 𝑥 ∈ On → ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ ( 𝐸 ∈ No ∧ 𝐹 ∈ No ) ) → ( 𝑥 = ( ( ( 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 𝐸 ) ) ) ) ) ) )
244	243	com23	⊢ ( 𝑥 ∈ On → ( 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ ( 𝐸 ∈ No ∧ 𝐹 ∈ No ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) ) ) )
245	244	rexlimiv	⊢ ( ∃ 𝑥 ∈ On 𝑥 = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ ( 𝐸 ∈ No ∧ 𝐹 ∈ No ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) ) )
246	22 245	ax-mp	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 𝐶 ∈ No ∧ 𝐷 ∈ No ) ∧ ( 𝐸 ∈ No ∧ 𝐹 ∈ No ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 𝐶 <s 𝐷 ∧ 𝐸 <s 𝐹 ) → ( ( 𝐶 ·s 𝐹 ) -s ( 𝐶 ·s 𝐸 ) ) <s ( ( 𝐷 ·s 𝐹 ) -s ( 𝐷 ·s 𝐸 ) ) ) ) )