Metamath Proof Explorer

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 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No ∧ D ∈ No ∧ E ∈ No ∧ F ∈ No → A ⋅ s B ∈ No ∧ C < s D ∧ E < s F → C ⋅ s F - s C ⋅ s E < s D ⋅ s F - s D ⋅ s E

Proof

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