Metamath Proof Explorer

Theorem addsproplem7

Description: Lemma for surreal addition properties. Putting together the three previous lemmas, we now show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsproplem.1 ⊢ φ → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
addspropord.2 ⊢ φ → X ∈ No
addspropord.3 ⊢ φ → Y ∈ No
addspropord.4 ⊢ φ → Z ∈ No
addspropord.5 ⊢ φ → Y < s Z
Assertion addsproplem7 ⊢ φ → Y + s X < s Z + s X

Proof

Step Hyp Ref Expression
1 addsproplem.1 ⊢ φ → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
2 addspropord.2 ⊢ φ → X ∈ No
3 addspropord.3 ⊢ φ → Y ∈ No
4 addspropord.4 ⊢ φ → Z ∈ No
5 addspropord.5 ⊢ φ → Y < s Z
6 bdayelon ⊢ bday ⁡ Y ∈ On
7 fvex ⊢ bday ⁡ Y ∈ V
8 7 elon ⊢ bday ⁡ Y ∈ On ↔ Ord ⁡ bday ⁡ Y
9 6 8 mpbi ⊢ Ord ⁡ bday ⁡ Y
10 bdayelon ⊢ bday ⁡ Z ∈ On
11 fvex ⊢ bday ⁡ Z ∈ V
12 11 elon ⊢ bday ⁡ Z ∈ On ↔ Ord ⁡ bday ⁡ Z
13 10 12 mpbi ⊢ Ord ⁡ bday ⁡ Z
14 ordtri3or ⊢ Ord ⁡ bday ⁡ Y ∧ Ord ⁡ bday ⁡ Z → bday ⁡ Y ∈ bday ⁡ Z ∨ bday ⁡ Y = bday ⁡ Z ∨ bday ⁡ Z ∈ bday ⁡ Y
15 9 13 14 mp2an ⊢ bday ⁡ Y ∈ bday ⁡ Z ∨ bday ⁡ Y = bday ⁡ Z ∨ bday ⁡ Z ∈ bday ⁡ Y
16 simpl ⊢ φ ∧ bday ⁡ Y ∈ bday ⁡ Z → φ
17 16 1 syl ⊢ φ ∧ bday ⁡ Y ∈ bday ⁡ Z → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
18 16 2 syl ⊢ φ ∧ bday ⁡ Y ∈ bday ⁡ Z → X ∈ No
19 16 3 syl ⊢ φ ∧ bday ⁡ Y ∈ bday ⁡ Z → Y ∈ No
20 16 4 syl ⊢ φ ∧ bday ⁡ Y ∈ bday ⁡ Z → Z ∈ No
21 16 5 syl ⊢ φ ∧ bday ⁡ Y ∈ bday ⁡ Z → Y < s Z
22 simpr ⊢ φ ∧ bday ⁡ Y ∈ bday ⁡ Z → bday ⁡ Y ∈ bday ⁡ Z
23 17 18 19 20 21 22 addsproplem4 ⊢ φ ∧ bday ⁡ Y ∈ bday ⁡ Z → Y + s X < s Z + s X
24 23 ex ⊢ φ → bday ⁡ Y ∈ bday ⁡ Z → Y + s X < s Z + s X
25 simpl ⊢ φ ∧ bday ⁡ Y = bday ⁡ Z → φ
26 25 1 syl ⊢ φ ∧ bday ⁡ Y = bday ⁡ Z → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
27 25 2 syl ⊢ φ ∧ bday ⁡ Y = bday ⁡ Z → X ∈ No
28 25 3 syl ⊢ φ ∧ bday ⁡ Y = bday ⁡ Z → Y ∈ No
29 25 4 syl ⊢ φ ∧ bday ⁡ Y = bday ⁡ Z → Z ∈ No
30 25 5 syl ⊢ φ ∧ bday ⁡ Y = bday ⁡ Z → Y < s Z
31 simpr ⊢ φ ∧ bday ⁡ Y = bday ⁡ Z → bday ⁡ Y = bday ⁡ Z
32 26 27 28 29 30 31 addsproplem6 ⊢ φ ∧ bday ⁡ Y = bday ⁡ Z → Y + s X < s Z + s X
33 32 ex ⊢ φ → bday ⁡ Y = bday ⁡ Z → Y + s X < s Z + s X
34 1 adantr ⊢ φ ∧ bday ⁡ Z ∈ bday ⁡ Y → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
35 2 adantr ⊢ φ ∧ bday ⁡ Z ∈ bday ⁡ Y → X ∈ No
36 3 adantr ⊢ φ ∧ bday ⁡ Z ∈ bday ⁡ Y → Y ∈ No
37 4 adantr ⊢ φ ∧ bday ⁡ Z ∈ bday ⁡ Y → Z ∈ No
38 5 adantr ⊢ φ ∧ bday ⁡ Z ∈ bday ⁡ Y → Y < s Z
39 simpr ⊢ φ ∧ bday ⁡ Z ∈ bday ⁡ Y → bday ⁡ Z ∈ bday ⁡ Y
40 34 35 36 37 38 39 addsproplem5 ⊢ φ ∧ bday ⁡ Z ∈ bday ⁡ Y → Y + s X < s Z + s X
41 40 ex ⊢ φ → bday ⁡ Z ∈ bday ⁡ Y → Y + s X < s Z + s X
42 24 33 41 3jaod ⊢ φ → bday ⁡ Y ∈ bday ⁡ Z ∨ bday ⁡ Y = bday ⁡ Z ∨ bday ⁡ Z ∈ bday ⁡ Y → Y + s X < s Z + s X
43 15 42 mpi ⊢ φ → Y + s X < s Z + s X