Metamath Proof Explorer

Theorem addsprop

Description: Inductively show that surreal addition is closed and compatible with less-than. This proof follows from induction on the birthdays of the surreal numbers involved. This pattern occurs throughout surreal development. Theorem 3.1 of Gonshor p. 14. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion addsprop ⊢ X ∈ No ∧ Y ∈ No ∧ Z ∈ No → X + s Y ∈ No ∧ Y < s Z → Y + s X < s Z + s X

Proof

Step Hyp Ref Expression
1 bdayelon ⊢ bday ⁡ X ∈ On
2 bdayelon ⊢ bday ⁡ Y ∈ On
3 naddcl ⊢ bday ⁡ X ∈ On ∧ bday ⁡ Y ∈ On → bday ⁡ X + bday ⁡ Y ∈ On
4 1 2 3 mp2an ⊢ bday ⁡ X + bday ⁡ Y ∈ On
5 bdayelon ⊢ bday ⁡ Z ∈ On
6 naddcl ⊢ bday ⁡ X ∈ On ∧ bday ⁡ Z ∈ On → bday ⁡ X + bday ⁡ Z ∈ On
7 1 5 6 mp2an ⊢ bday ⁡ X + bday ⁡ Z ∈ On
8 4 7 onun2i ⊢ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z ∈ On
9 risset ⊢ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z ∈ On ↔ ∃ a ∈ On a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
10 8 9 mpbi ⊢ ∃ a ∈ On a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
11 eqeq1 ⊢ a = b → a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ↔ b = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z
12 11 imbi1d ⊢ a = b → a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ b = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
13 12 ralbidv ⊢ a = b → ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ ∀ z ∈ No b = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
14 13 2ralbidv ⊢ a = b → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No b = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
15 fveq2 ⊢ x = p → bday ⁡ x = bday ⁡ p
16 15 oveq1d ⊢ x = p → bday ⁡ x + bday ⁡ y = bday ⁡ p + bday ⁡ y
17 15 oveq1d ⊢ x = p → bday ⁡ x + bday ⁡ z = bday ⁡ p + bday ⁡ z
18 16 17 uneq12d ⊢ x = p → bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z = bday ⁡ p + bday ⁡ y ∪ bday ⁡ p + bday ⁡ z
19 18 eqeq2d ⊢ x = p → b = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ↔ b = bday ⁡ p + bday ⁡ y ∪ bday ⁡ p + bday ⁡ z
20 oveq1 ⊢ x = p → x + s y = p + s y
21 20 eleq1d ⊢ x = p → x + s y ∈ No ↔ p + s y ∈ No
22 oveq2 ⊢ x = p → y + s x = y + s p
23 oveq2 ⊢ x = p → z + s x = z + s p
24 22 23 breq12d ⊢ x = p → y + s x < s z + s x ↔ y + s p < s z + s p
25 24 imbi2d ⊢ x = p → y < s z → y + s x < s z + s x ↔ y < s z → y + s p < s z + s p
26 21 25 anbi12d ⊢ x = p → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ p + s y ∈ No ∧ y < s z → y + s p < s z + s p
27 19 26 imbi12d ⊢ x = p → b = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ b = bday ⁡ p + bday ⁡ y ∪ bday ⁡ p + bday ⁡ z → p + s y ∈ No ∧ y < s z → y + s p < s z + s p
28 fveq2 ⊢ y = q → bday ⁡ y = bday ⁡ q
29 28 oveq2d ⊢ y = q → bday ⁡ p + bday ⁡ y = bday ⁡ p + bday ⁡ q
30 29 uneq1d ⊢ y = q → bday ⁡ p + bday ⁡ y ∪ bday ⁡ p + bday ⁡ z = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ z
31 30 eqeq2d ⊢ y = q → b = bday ⁡ p + bday ⁡ y ∪ bday ⁡ p + bday ⁡ z ↔ b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ z
32 oveq2 ⊢ y = q → p + s y = p + s q
33 32 eleq1d ⊢ y = q → p + s y ∈ No ↔ p + s q ∈ No
34 breq1 ⊢ y = q → y < s z ↔ q < s z
35 oveq1 ⊢ y = q → y + s p = q + s p
36 35 breq1d ⊢ y = q → y + s p < s z + s p ↔ q + s p < s z + s p
37 34 36 imbi12d ⊢ y = q → y < s z → y + s p < s z + s p ↔ q < s z → q + s p < s z + s p
38 33 37 anbi12d ⊢ y = q → p + s y ∈ No ∧ y < s z → y + s p < s z + s p ↔ p + s q ∈ No ∧ q < s z → q + s p < s z + s p
39 31 38 imbi12d ⊢ y = q → b = bday ⁡ p + bday ⁡ y ∪ bday ⁡ p + bday ⁡ z → p + s y ∈ No ∧ y < s z → y + s p < s z + s p ↔ b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ z → p + s q ∈ No ∧ q < s z → q + s p < s z + s p
40 fveq2 ⊢ z = r → bday ⁡ z = bday ⁡ r
41 40 oveq2d ⊢ z = r → bday ⁡ p + bday ⁡ z = bday ⁡ p + bday ⁡ r
42 41 uneq2d ⊢ z = r → bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ z = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r
43 42 eqeq2d ⊢ z = r → b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ z ↔ b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r
44 breq2 ⊢ z = r → q < s z ↔ q < s r
45 oveq1 ⊢ z = r → z + s p = r + s p
46 45 breq2d ⊢ z = r → q + s p < s z + s p ↔ q + s p < s r + s p
47 44 46 imbi12d ⊢ z = r → q < s z → q + s p < s z + s p ↔ q < s r → q + s p < s r + s p
48 47 anbi2d ⊢ z = r → p + s q ∈ No ∧ q < s z → q + s p < s z + s p ↔ p + s q ∈ No ∧ q < s r → q + s p < s r + s p
49 43 48 imbi12d ⊢ z = r → b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ z → p + s q ∈ No ∧ q < s z → q + s p < s z + s p ↔ b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
50 27 39 49 cbvral3vw ⊢ ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No b = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
51 14 50 bitrdi ⊢ a = b → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
52 ralrot3 ⊢ ∀ p ∈ No ∀ q ∈ No ∀ b ∈ a ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∀ b ∈ a ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
53 ralcom ⊢ ∀ b ∈ a ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∀ r ∈ No ∀ b ∈ a b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
54 r19.23v ⊢ ∀ b ∈ a b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∃ b ∈ a b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
55 risset ⊢ bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a ↔ ∃ b ∈ a b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r
56 55 imbi1i ⊢ bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∃ b ∈ a b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
57 54 56 bitr4i ⊢ ∀ b ∈ a b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
58 57 ralbii ⊢ ∀ r ∈ No ∀ b ∈ a b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
59 53 58 bitri ⊢ ∀ b ∈ a ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
60 59 2ralbii ⊢ ∀ p ∈ No ∀ q ∈ No ∀ b ∈ a ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
61 52 60 bitr3i ⊢ ∀ b ∈ a ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
62 eleq2 ⊢ a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a ↔ bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z
63 62 imbi1d ⊢ a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
64 63 ralbidv ⊢ a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
65 64 2ralbidv ⊢ a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ↔ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
66 65 anbi1d ⊢ a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No ↔ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No
67 66 biimpcd ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No
68 simpl ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
69 simprll ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → x ∈ No
70 simprlr ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → y ∈ No
71 68 69 70 addsproplem3 ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → x + s y ∈ No ∧ a | ∃ b ∈ L ⁡ x a = b + s y ∪ c | ∃ d ∈ L ⁡ y c = x + s d ≪ s x + s y ∧ x + s y ≪ s e | ∃ f ∈ R ⁡ x e = f + s y ∪ g | ∃ h ∈ R ⁡ y g = x + s h
72 71 simp1d ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → x + s y ∈ No
73 68 adantr ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No ∧ y < s z → ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p
74 69 adantr ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No ∧ y < s z → x ∈ No
75 70 adantr ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No ∧ y < s z → y ∈ No
76 simplrr ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No ∧ y < s z → z ∈ No
77 simpr ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No ∧ y < s z → y < s z
78 73 74 75 76 77 addsproplem7 ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No ∧ y < s z → y + s x < s z + s x
79 78 ex ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → y < s z → y + s x < s z + s x
80 72 79 jca ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
81 67 80 syl6 ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
82 81 anassrs ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No ∧ z ∈ No → a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
83 82 ralrimiva ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p ∧ x ∈ No ∧ y ∈ No → ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
84 83 ralrimivva ⊢ ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r ∈ a → p + s q ∈ No ∧ q < s r → q + s p < s r + s p → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
85 61 84 sylbi ⊢ ∀ b ∈ a ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
86 85 a1i ⊢ a ∈ On → ∀ b ∈ a ∀ p ∈ No ∀ q ∈ No ∀ r ∈ No b = bday ⁡ p + bday ⁡ q ∪ bday ⁡ p + bday ⁡ r → p + s q ∈ No ∧ q < s r → q + s p < s r + s p → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
87 51 86 tfis2 ⊢ a ∈ On → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
88 fveq2 ⊢ x = X → bday ⁡ x = bday ⁡ X
89 88 oveq1d ⊢ x = X → bday ⁡ x + bday ⁡ y = bday ⁡ X + bday ⁡ y
90 88 oveq1d ⊢ x = X → bday ⁡ x + bday ⁡ z = bday ⁡ X + bday ⁡ z
91 89 90 uneq12d ⊢ x = X → bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z = bday ⁡ X + bday ⁡ y ∪ bday ⁡ X + bday ⁡ z
92 91 eqeq2d ⊢ x = X → a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ↔ a = bday ⁡ X + bday ⁡ y ∪ bday ⁡ X + bday ⁡ z
93 oveq1 ⊢ x = X → x + s y = X + s y
94 93 eleq1d ⊢ x = X → x + s y ∈ No ↔ X + s y ∈ No
95 oveq2 ⊢ x = X → y + s x = y + s X
96 oveq2 ⊢ x = X → z + s x = z + s X
97 95 96 breq12d ⊢ x = X → y + s x < s z + s x ↔ y + s X < s z + s X
98 97 imbi2d ⊢ x = X → y < s z → y + s x < s z + s x ↔ y < s z → y + s X < s z + s X
99 94 98 anbi12d ⊢ x = X → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ X + s y ∈ No ∧ y < s z → y + s X < s z + s X
100 92 99 imbi12d ⊢ x = X → a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ a = bday ⁡ X + bday ⁡ y ∪ bday ⁡ X + bday ⁡ z → X + s y ∈ No ∧ y < s z → y + s X < s z + s X
101 fveq2 ⊢ y = Y → bday ⁡ y = bday ⁡ Y
102 101 oveq2d ⊢ y = Y → bday ⁡ X + bday ⁡ y = bday ⁡ X + bday ⁡ Y
103 102 uneq1d ⊢ y = Y → bday ⁡ X + bday ⁡ y ∪ bday ⁡ X + bday ⁡ z = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ z
104 103 eqeq2d ⊢ y = Y → a = bday ⁡ X + bday ⁡ y ∪ bday ⁡ X + bday ⁡ z ↔ a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ z
105 oveq2 ⊢ y = Y → X + s y = X + s Y
106 105 eleq1d ⊢ y = Y → X + s y ∈ No ↔ X + s Y ∈ No
107 breq1 ⊢ y = Y → y < s z ↔ Y < s z
108 oveq1 ⊢ y = Y → y + s X = Y + s X
109 108 breq1d ⊢ y = Y → y + s X < s z + s X ↔ Y + s X < s z + s X
110 107 109 imbi12d ⊢ y = Y → y < s z → y + s X < s z + s X ↔ Y < s z → Y + s X < s z + s X
111 106 110 anbi12d ⊢ y = Y → X + s y ∈ No ∧ y < s z → y + s X < s z + s X ↔ X + s Y ∈ No ∧ Y < s z → Y + s X < s z + s X
112 104 111 imbi12d ⊢ y = Y → a = bday ⁡ X + bday ⁡ y ∪ bday ⁡ X + bday ⁡ z → X + s y ∈ No ∧ y < s z → y + s X < s z + s X ↔ a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ z → X + s Y ∈ No ∧ Y < s z → Y + s X < s z + s X
113 fveq2 ⊢ z = Z → bday ⁡ z = bday ⁡ Z
114 113 oveq2d ⊢ z = Z → bday ⁡ X + bday ⁡ z = bday ⁡ X + bday ⁡ Z
115 114 uneq2d ⊢ z = Z → bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ z = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
116 115 eqeq2d ⊢ z = Z → a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ z ↔ a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
117 breq2 ⊢ z = Z → Y < s z ↔ Y < s Z
118 oveq1 ⊢ z = Z → z + s X = Z + s X
119 118 breq2d ⊢ z = Z → Y + s X < s z + s X ↔ Y + s X < s Z + s X
120 117 119 imbi12d ⊢ z = Z → Y < s z → Y + s X < s z + s X ↔ Y < s Z → Y + s X < s Z + s X
121 120 anbi2d ⊢ z = Z → X + s Y ∈ No ∧ Y < s z → Y + s X < s z + s X ↔ X + s Y ∈ No ∧ Y < s Z → Y + s X < s Z + s X
122 116 121 imbi12d ⊢ z = Z → a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ z → X + s Y ∈ No ∧ Y < s z → Y + s X < s z + s X ↔ a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → X + s Y ∈ No ∧ Y < s Z → Y + s X < s Z + s X
123 100 112 122 rspc3v ⊢ X ∈ No ∧ Y ∈ No ∧ Z ∈ No → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No a = bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x → a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → X + s Y ∈ No ∧ Y < s Z → Y + s X < s Z + s X
124 87 123 syl5com ⊢ a ∈ On → X ∈ No ∧ Y ∈ No ∧ Z ∈ No → a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → X + s Y ∈ No ∧ Y < s Z → Y + s X < s Z + s X
125 124 com23 ⊢ a ∈ On → a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → X ∈ No ∧ Y ∈ No ∧ Z ∈ No → X + s Y ∈ No ∧ Y < s Z → Y + s X < s Z + s X
126 125 rexlimiv ⊢ ∃ a ∈ On a = bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → X ∈ No ∧ Y ∈ No ∧ Z ∈ No → X + s Y ∈ No ∧ Y < s Z → Y + s X < s Z + s X
127 10 126 ax-mp ⊢ X ∈ No ∧ Y ∈ No ∧ Z ∈ No → X + s Y ∈ No ∧ Y < s Z → Y + s X < s Z + s X