Metamath Proof Explorer

Theorem addsproplem4

Description: Lemma for surreal addition properties. Show the second half of the inductive hypothesis when Y is older than Z . (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
addsproplem4.6 ⊢ φ → bday ⁡ Y ∈ bday ⁡ Z
Assertion addsproplem4 ⊢ φ → 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 addsproplem4.6 ⊢ φ → bday ⁡ Y ∈ bday ⁡ Z
7 uncom ⊢ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z = bday ⁡ X + bday ⁡ Z ∪ bday ⁡ X + bday ⁡ Y
8 7 eleq2i ⊢ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z ↔ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Z ∪ bday ⁡ X + bday ⁡ Y
9 8 imbi1i ⊢ 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 ↔ bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Z ∪ bday ⁡ X + bday ⁡ Y → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
10 9 ralbii ⊢ ∀ 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 ↔ ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Z ∪ bday ⁡ X + bday ⁡ Y → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
11 10 2ralbii ⊢ ∀ 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 ↔ ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Z ∪ bday ⁡ X + bday ⁡ Y → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
12 1 11 sylib ⊢ φ → ∀ x ∈ No ∀ y ∈ No ∀ z ∈ No bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Z ∪ bday ⁡ X + bday ⁡ Y → x + s y ∈ No ∧ y < s z → y + s x < s z + s x
13 12 2 4 addsproplem3 ⊢ φ → X + s Z ∈ No ∧ a | ∃ c ∈ L ⁡ X a = c + s Z ∪ b | ∃ d ∈ L ⁡ Z b = X + s d ≪ s X + s Z ∧ X + s Z ≪ s e | ∃ g ∈ R ⁡ X e = g + s Z ∪ f | ∃ h ∈ R ⁡ Z f = X + s h
14 13 simp2d ⊢ φ → a | ∃ c ∈ L ⁡ X a = c + s Z ∪ b | ∃ d ∈ L ⁡ Z b = X + s d ≪ s X + s Z
15 bdayelon ⊢ bday ⁡ Z ∈ On
16 oldbday ⊢ bday ⁡ Z ∈ On ∧ Y ∈ No → Y ∈ Old ⁡ bday ⁡ Z ↔ bday ⁡ Y ∈ bday ⁡ Z
17 15 3 16 sylancr ⊢ φ → Y ∈ Old ⁡ bday ⁡ Z ↔ bday ⁡ Y ∈ bday ⁡ Z
18 6 17 mpbird ⊢ φ → Y ∈ Old ⁡ bday ⁡ Z
19 breq1 ⊢ y = Y → y < s Z ↔ Y < s Z
20 leftval ⊢ L ⁡ Z = y ∈ Old ⁡ bday ⁡ Z | y < s Z
21 19 20 elrab2 ⊢ Y ∈ L ⁡ Z ↔ Y ∈ Old ⁡ bday ⁡ Z ∧ Y < s Z
22 18 5 21 sylanbrc ⊢ φ → Y ∈ L ⁡ Z
23 eqid ⊢ X + s Y = X + s Y
24 oveq2 ⊢ d = Y → X + s d = X + s Y
25 24 rspceeqv ⊢ Y ∈ L ⁡ Z ∧ X + s Y = X + s Y → ∃ d ∈ L ⁡ Z X + s Y = X + s d
26 22 23 25 sylancl ⊢ φ → ∃ d ∈ L ⁡ Z X + s Y = X + s d
27 ovex ⊢ X + s Y ∈ V
28 eqeq1 ⊢ b = X + s Y → b = X + s d ↔ X + s Y = X + s d
29 28 rexbidv ⊢ b = X + s Y → ∃ d ∈ L ⁡ Z b = X + s d ↔ ∃ d ∈ L ⁡ Z X + s Y = X + s d
30 27 29 elab ⊢ X + s Y ∈ b | ∃ d ∈ L ⁡ Z b = X + s d ↔ ∃ d ∈ L ⁡ Z X + s Y = X + s d
31 26 30 sylibr ⊢ φ → X + s Y ∈ b | ∃ d ∈ L ⁡ Z b = X + s d
32 elun2 ⊢ X + s Y ∈ b | ∃ d ∈ L ⁡ Z b = X + s d → X + s Y ∈ a | ∃ c ∈ L ⁡ X a = c + s Z ∪ b | ∃ d ∈ L ⁡ Z b = X + s d
33 31 32 syl ⊢ φ → X + s Y ∈ a | ∃ c ∈ L ⁡ X a = c + s Z ∪ b | ∃ d ∈ L ⁡ Z b = X + s d
34 ovex ⊢ X + s Z ∈ V
35 34 snid ⊢ X + s Z ∈ X + s Z
36 35 a1i ⊢ φ → X + s Z ∈ X + s Z
37 14 33 36 ssltsepcd ⊢ φ → X + s Y < s X + s Z
38 3 2 addscomd ⊢ φ → Y + s X = X + s Y
39 4 2 addscomd ⊢ φ → Z + s X = X + s Z
40 37 38 39 3brtr4d ⊢ φ → Y + s X < s Z + s X