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 elleft ⊢ Y ∈ L ⁡ Z ↔ Y ∈ Old ⁡ bday ⁡ Z ∧ Y < s Z
20 18 5 19 sylanbrc ⊢ φ → Y ∈ L ⁡ Z
21 eqid ⊢ X + s Y = X + s Y
22 oveq2 ⊢ d = Y → X + s d = X + s Y
23 22 rspceeqv ⊢ Y ∈ L ⁡ Z ∧ X + s Y = X + s Y → ∃ d ∈ L ⁡ Z X + s Y = X + s d
24 20 21 23 sylancl ⊢ φ → ∃ d ∈ L ⁡ Z X + s Y = X + s d
25 ovex ⊢ X + s Y ∈ V
26 eqeq1 ⊢ b = X + s Y → b = X + s d ↔ X + s Y = X + s d
27 26 rexbidv ⊢ b = X + s Y → ∃ d ∈ L ⁡ Z b = X + s d ↔ ∃ d ∈ L ⁡ Z X + s Y = X + s d
28 25 27 elab ⊢ X + s Y ∈ b | ∃ d ∈ L ⁡ Z b = X + s d ↔ ∃ d ∈ L ⁡ Z X + s Y = X + s d
29 24 28 sylibr ⊢ φ → X + s Y ∈ b | ∃ d ∈ L ⁡ Z b = X + s d
30 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
31 29 30 syl ⊢ φ → X + s Y ∈ a | ∃ c ∈ L ⁡ X a = c + s Z ∪ b | ∃ d ∈ L ⁡ Z b = X + s d
32 ovex ⊢ X + s Z ∈ V
33 32 snid ⊢ X + s Z ∈ X + s Z
34 33 a1i ⊢ φ → X + s Z ∈ X + s Z
35 14 31 34 ssltsepcd ⊢ φ → X + s Y < s X + s Z
36 3 2 addscomd ⊢ φ → Y + s X = X + s Y
37 4 2 addscomd ⊢ φ → Z + s X = X + s Z
38 35 36 37 3brtr4d ⊢ φ → Y + s X < s Z + s X