Metamath Proof Explorer


Theorem mulsproplemcbv

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

Ref Expression
Hypothesis 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 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 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mulsproplem.1 ( 𝜑 → ∀ 𝑎 No 𝑏 No 𝑐 No 𝑑 No 𝑒 No 𝑓 No ( ( ( ( bday 𝑎 ) +no ( bday 𝑏 ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑐 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
2 fveq2 ( 𝑎 = 𝑔 → ( bday 𝑎 ) = ( bday 𝑔 ) )
3 2 oveq1d ( 𝑎 = 𝑔 → ( ( bday 𝑎 ) +no ( bday 𝑏 ) ) = ( ( bday 𝑔 ) +no ( bday 𝑏 ) ) )
4 3 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 𝑒 ) ) ) ) ) )
5 4 eleq1d ( 𝑎 = 𝑔 → ( ( ( ( bday 𝑎 ) +no ( bday 𝑏 ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑐 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ↔ ( ( ( bday 𝑔 ) +no ( bday 𝑏 ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑐 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ) )
6 oveq1 ( 𝑎 = 𝑔 → ( 𝑎 ·s 𝑏 ) = ( 𝑔 ·s 𝑏 ) )
7 6 eleq1d ( 𝑎 = 𝑔 → ( ( 𝑎 ·s 𝑏 ) ∈ No ↔ ( 𝑔 ·s 𝑏 ) ∈ No ) )
8 7 anbi1d ( 𝑎 = 𝑔 → ( ( ( 𝑎 ·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 ( 𝑎 = 𝑔 → ( ( ( ( ( bday 𝑎 ) +no ( bday 𝑏 ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( 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 ( 𝑏 = → ( bday 𝑏 ) = ( bday ) )
11 10 oveq2d ( 𝑏 = → ( ( bday 𝑔 ) +no ( bday 𝑏 ) ) = ( ( bday 𝑔 ) +no ( bday ) ) )
12 11 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 𝑒 ) ) ) ) ) )
13 12 eleq1d ( 𝑏 = → ( ( ( ( bday 𝑔 ) +no ( bday 𝑏 ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑐 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ↔ ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑐 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ) )
14 oveq2 ( 𝑏 = → ( 𝑔 ·s 𝑏 ) = ( 𝑔 ·s ) )
15 14 eleq1d ( 𝑏 = → ( ( 𝑔 ·s 𝑏 ) ∈ No ↔ ( 𝑔 ·s ) ∈ No ) )
16 15 anbi1d ( 𝑏 = → ( ( ( 𝑔 ·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 ( 𝑏 = → ( ( ( ( ( bday 𝑔 ) +no ( bday 𝑏 ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( 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 ( 𝑐 = 𝑖 → ( bday 𝑐 ) = ( bday 𝑖 ) )
19 18 oveq1d ( 𝑐 = 𝑖 → ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) = ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) )
20 19 uneq1d ( 𝑐 = 𝑖 → ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) = ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) )
21 18 oveq1d ( 𝑐 = 𝑖 → ( ( bday 𝑐 ) +no ( bday 𝑓 ) ) = ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) )
22 21 uneq1d ( 𝑐 = 𝑖 → ( ( ( bday 𝑐 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) = ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) )
23 20 22 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 𝑒 ) ) ) ) )
24 23 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 𝑒 ) ) ) ) ) )
25 24 eleq1d ( 𝑐 = 𝑖 → ( ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑐 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ↔ ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ) )
26 breq1 ( 𝑐 = 𝑖 → ( 𝑐 <s 𝑑𝑖 <s 𝑑 ) )
27 26 anbi1d ( 𝑐 = 𝑖 → ( ( 𝑐 <s 𝑑𝑒 <s 𝑓 ) ↔ ( 𝑖 <s 𝑑𝑒 <s 𝑓 ) ) )
28 oveq1 ( 𝑐 = 𝑖 → ( 𝑐 ·s 𝑓 ) = ( 𝑖 ·s 𝑓 ) )
29 oveq1 ( 𝑐 = 𝑖 → ( 𝑐 ·s 𝑒 ) = ( 𝑖 ·s 𝑒 ) )
30 28 29 oveq12d ( 𝑐 = 𝑖 → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) = ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) )
31 30 breq1d ( 𝑐 = 𝑖 → ( ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ↔ ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) )
32 27 31 imbi12d ( 𝑐 = 𝑖 → ( ( ( 𝑐 <s 𝑑𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ↔ ( ( 𝑖 <s 𝑑𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) )
33 32 anbi2d ( 𝑐 = 𝑖 → ( ( ( 𝑔 ·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 ( 𝑐 = 𝑖 → ( ( ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑐 ) +no ( bday 𝑒 ) ) ∪ ( ( 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 ( 𝑑 = 𝑗 → ( bday 𝑑 ) = ( bday 𝑗 ) )
36 35 oveq1d ( 𝑑 = 𝑗 → ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) = ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) )
37 36 uneq2d ( 𝑑 = 𝑗 → ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) = ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) ) )
38 35 oveq1d ( 𝑑 = 𝑗 → ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) = ( ( bday 𝑗 ) +no ( bday 𝑒 ) ) )
39 38 uneq2d ( 𝑑 = 𝑗 → ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) = ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑒 ) ) ) )
40 37 39 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 𝑒 ) ) ) ) )
41 40 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 𝑒 ) ) ) ) ) )
42 41 eleq1d ( 𝑑 = 𝑗 → ( ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑑 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ↔ ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ) )
43 breq2 ( 𝑑 = 𝑗 → ( 𝑖 <s 𝑑𝑖 <s 𝑗 ) )
44 43 anbi1d ( 𝑑 = 𝑗 → ( ( 𝑖 <s 𝑑𝑒 <s 𝑓 ) ↔ ( 𝑖 <s 𝑗𝑒 <s 𝑓 ) ) )
45 oveq1 ( 𝑑 = 𝑗 → ( 𝑑 ·s 𝑓 ) = ( 𝑗 ·s 𝑓 ) )
46 oveq1 ( 𝑑 = 𝑗 → ( 𝑑 ·s 𝑒 ) = ( 𝑗 ·s 𝑒 ) )
47 45 46 oveq12d ( 𝑑 = 𝑗 → ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) = ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) )
48 47 breq2d ( 𝑑 = 𝑗 → ( ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ↔ ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) )
49 44 48 imbi12d ( 𝑑 = 𝑗 → ( ( ( 𝑖 <s 𝑑𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ↔ ( ( 𝑖 <s 𝑗𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) ) )
50 49 anbi2d ( 𝑑 = 𝑗 → ( ( ( 𝑔 ·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 ( 𝑑 = 𝑗 → ( ( ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( 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 ( 𝑒 = 𝑘 → ( bday 𝑒 ) = ( bday 𝑘 ) )
53 52 oveq2d ( 𝑒 = 𝑘 → ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) = ( ( bday 𝑖 ) +no ( bday 𝑘 ) ) )
54 53 uneq1d ( 𝑒 = 𝑘 → ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) ) = ( ( ( bday 𝑖 ) +no ( bday 𝑘 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) ) )
55 52 oveq2d ( 𝑒 = 𝑘 → ( ( bday 𝑗 ) +no ( bday 𝑒 ) ) = ( ( bday 𝑗 ) +no ( bday 𝑘 ) ) )
56 55 uneq2d ( 𝑒 = 𝑘 → ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑒 ) ) ) = ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑘 ) ) ) )
57 54 56 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 𝑘 ) ) ) ) )
58 57 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 𝑘 ) ) ) ) ) )
59 58 eleq1d ( 𝑒 = 𝑘 → ( ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑒 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ↔ ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑘 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑘 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ) )
60 breq1 ( 𝑒 = 𝑘 → ( 𝑒 <s 𝑓𝑘 <s 𝑓 ) )
61 60 anbi2d ( 𝑒 = 𝑘 → ( ( 𝑖 <s 𝑗𝑒 <s 𝑓 ) ↔ ( 𝑖 <s 𝑗𝑘 <s 𝑓 ) ) )
62 oveq2 ( 𝑒 = 𝑘 → ( 𝑖 ·s 𝑒 ) = ( 𝑖 ·s 𝑘 ) )
63 62 oveq2d ( 𝑒 = 𝑘 → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) = ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) )
64 oveq2 ( 𝑒 = 𝑘 → ( 𝑗 ·s 𝑒 ) = ( 𝑗 ·s 𝑘 ) )
65 64 oveq2d ( 𝑒 = 𝑘 → ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) = ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) )
66 63 65 breq12d ( 𝑒 = 𝑘 → ( ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ↔ ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) )
67 61 66 imbi12d ( 𝑒 = 𝑘 → ( ( ( 𝑖 <s 𝑗𝑒 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑒 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑒 ) ) ) ↔ ( ( 𝑖 <s 𝑗𝑘 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) )
68 67 anbi2d ( 𝑒 = 𝑘 → ( ( ( 𝑔 ·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 ( 𝑒 = 𝑘 → ( ( ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑒 ) ) ∪ ( ( 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 ( 𝑓 = 𝑙 → ( bday 𝑓 ) = ( bday 𝑙 ) )
71 70 oveq2d ( 𝑓 = 𝑙 → ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) = ( ( bday 𝑗 ) +no ( bday 𝑙 ) ) )
72 71 uneq2d ( 𝑓 = 𝑙 → ( ( ( bday 𝑖 ) +no ( bday 𝑘 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) ) = ( ( ( bday 𝑖 ) +no ( bday 𝑘 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑙 ) ) ) )
73 70 oveq2d ( 𝑓 = 𝑙 → ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) = ( ( bday 𝑖 ) +no ( bday 𝑙 ) ) )
74 73 uneq1d ( 𝑓 = 𝑙 → ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑘 ) ) ) = ( ( ( bday 𝑖 ) +no ( bday 𝑙 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑘 ) ) ) )
75 72 74 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 𝑘 ) ) ) ) )
76 75 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 𝑘 ) ) ) ) ) )
77 76 eleq1d ( 𝑓 = 𝑙 → ( ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑘 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑓 ) ) ) ∪ ( ( ( bday 𝑖 ) +no ( bday 𝑓 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑘 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ↔ ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑘 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑙 ) ) ) ∪ ( ( ( bday 𝑖 ) +no ( bday 𝑙 ) ) ∪ ( ( bday 𝑗 ) +no ( bday 𝑘 ) ) ) ) ) ∈ ( ( ( bday 𝐴 ) +no ( bday 𝐵 ) ) ∪ ( ( ( ( bday 𝐶 ) +no ( bday 𝐸 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐹 ) ) ) ∪ ( ( ( bday 𝐶 ) +no ( bday 𝐹 ) ) ∪ ( ( bday 𝐷 ) +no ( bday 𝐸 ) ) ) ) ) ) )
78 breq2 ( 𝑓 = 𝑙 → ( 𝑘 <s 𝑓𝑘 <s 𝑙 ) )
79 78 anbi2d ( 𝑓 = 𝑙 → ( ( 𝑖 <s 𝑗𝑘 <s 𝑓 ) ↔ ( 𝑖 <s 𝑗𝑘 <s 𝑙 ) ) )
80 oveq2 ( 𝑓 = 𝑙 → ( 𝑖 ·s 𝑓 ) = ( 𝑖 ·s 𝑙 ) )
81 80 oveq1d ( 𝑓 = 𝑙 → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) = ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) )
82 oveq2 ( 𝑓 = 𝑙 → ( 𝑗 ·s 𝑓 ) = ( 𝑗 ·s 𝑙 ) )
83 82 oveq1d ( 𝑓 = 𝑙 → ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) = ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) )
84 81 83 breq12d ( 𝑓 = 𝑙 → ( ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ↔ ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) )
85 79 84 imbi12d ( 𝑓 = 𝑙 → ( ( ( 𝑖 <s 𝑗𝑘 <s 𝑓 ) → ( ( 𝑖 ·s 𝑓 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑓 ) -s ( 𝑗 ·s 𝑘 ) ) ) ↔ ( ( 𝑖 <s 𝑗𝑘 <s 𝑙 ) → ( ( 𝑖 ·s 𝑙 ) -s ( 𝑖 ·s 𝑘 ) ) <s ( ( 𝑗 ·s 𝑙 ) -s ( 𝑗 ·s 𝑘 ) ) ) ) )
86 85 anbi2d ( 𝑓 = 𝑙 → ( ( ( 𝑔 ·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 ( 𝑓 = 𝑙 → ( ( ( ( ( bday 𝑔 ) +no ( bday ) ) ∪ ( ( ( ( bday 𝑖 ) +no ( bday 𝑘 ) ) ∪ ( ( 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 ( ∀ 𝑎 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 ( 𝜑 → ∀ 𝑔 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 𝑘 ) ) ) ) ) )