Metamath Proof Explorer

Theorem addsproplem1

Description: Lemma for surreal addition properties. To prove closure on surreal addition we need to prove that addition is compatible with order at the same time. We do this by inducting over the maximum of two natural sums of the birthdays of surreals numbers. In the final step we will loop around and use tfr3 to prove this of all surreals. This first lemma just instantiates the inductive hypothesis so we do not need to do it continuously throughout the proof. (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
addsproplem1.2 ⊢ φ → A ∈ No
addsproplem1.3 ⊢ φ → B ∈ No
addsproplem1.4 ⊢ φ → C ∈ No
addsproplem1.5 ⊢ φ → bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ C ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
Assertion addsproplem1 ⊢ φ → A + s B ∈ No ∧ B < s C → B + s A < s C + s A

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 addsproplem1.2 ⊢ φ → A ∈ No
3 addsproplem1.3 ⊢ φ → B ∈ No
4 addsproplem1.4 ⊢ φ → C ∈ No
5 addsproplem1.5 ⊢ φ → bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ C ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
6 2 3 4 3jca ⊢ φ → A ∈ No ∧ B ∈ No ∧ C ∈ No
7 fveq2 ⊢ x = A → bday ⁡ x = bday ⁡ A
8 7 oveq1d ⊢ x = A → bday ⁡ x + bday ⁡ y = bday ⁡ A + bday ⁡ y
9 7 oveq1d ⊢ x = A → bday ⁡ x + bday ⁡ z = bday ⁡ A + bday ⁡ z
10 8 9 uneq12d ⊢ x = A → bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z = bday ⁡ A + bday ⁡ y ∪ bday ⁡ A + bday ⁡ z
11 10 eleq1d ⊢ x = A → bday ⁡ x + bday ⁡ y ∪ bday ⁡ x + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z ↔ bday ⁡ A + bday ⁡ y ∪ bday ⁡ A + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
12 oveq1 ⊢ x = A → x + s y = A + s y
13 12 eleq1d ⊢ x = A → x + s y ∈ No ↔ A + s y ∈ No
14 oveq2 ⊢ x = A → y + s x = y + s A
15 oveq2 ⊢ x = A → z + s x = z + s A
16 14 15 breq12d ⊢ x = A → y + s x < s z + s x ↔ y + s A < s z + s A
17 16 imbi2d ⊢ x = A → y < s z → y + s x < s z + s x ↔ y < s z → y + s A < s z + s A
18 13 17 anbi12d ⊢ x = A → x + s y ∈ No ∧ y < s z → y + s x < s z + s x ↔ A + s y ∈ No ∧ y < s z → y + s A < s z + s A
19 11 18 imbi12d ⊢ x = A → 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 ⁡ A + bday ⁡ y ∪ bday ⁡ A + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → A + s y ∈ No ∧ y < s z → y + s A < s z + s A
20 fveq2 ⊢ y = B → bday ⁡ y = bday ⁡ B
21 20 oveq2d ⊢ y = B → bday ⁡ A + bday ⁡ y = bday ⁡ A + bday ⁡ B
22 21 uneq1d ⊢ y = B → bday ⁡ A + bday ⁡ y ∪ bday ⁡ A + bday ⁡ z = bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ z
23 22 eleq1d ⊢ y = B → bday ⁡ A + bday ⁡ y ∪ bday ⁡ A + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z ↔ bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
24 oveq2 ⊢ y = B → A + s y = A + s B
25 24 eleq1d ⊢ y = B → A + s y ∈ No ↔ A + s B ∈ No
26 breq1 ⊢ y = B → y < s z ↔ B < s z
27 oveq1 ⊢ y = B → y + s A = B + s A
28 27 breq1d ⊢ y = B → y + s A < s z + s A ↔ B + s A < s z + s A
29 26 28 imbi12d ⊢ y = B → y < s z → y + s A < s z + s A ↔ B < s z → B + s A < s z + s A
30 25 29 anbi12d ⊢ y = B → A + s y ∈ No ∧ y < s z → y + s A < s z + s A ↔ A + s B ∈ No ∧ B < s z → B + s A < s z + s A
31 23 30 imbi12d ⊢ y = B → bday ⁡ A + bday ⁡ y ∪ bday ⁡ A + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → A + s y ∈ No ∧ y < s z → y + s A < s z + s A ↔ bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → A + s B ∈ No ∧ B < s z → B + s A < s z + s A
32 fveq2 ⊢ z = C → bday ⁡ z = bday ⁡ C
33 32 oveq2d ⊢ z = C → bday ⁡ A + bday ⁡ z = bday ⁡ A + bday ⁡ C
34 33 uneq2d ⊢ z = C → bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ z = bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ C
35 34 eleq1d ⊢ z = C → bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z ↔ bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ C ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
36 breq2 ⊢ z = C → B < s z ↔ B < s C
37 oveq1 ⊢ z = C → z + s A = C + s A
38 37 breq2d ⊢ z = C → B + s A < s z + s A ↔ B + s A < s C + s A
39 36 38 imbi12d ⊢ z = C → B < s z → B + s A < s z + s A ↔ B < s C → B + s A < s C + s A
40 39 anbi2d ⊢ z = C → A + s B ∈ No ∧ B < s z → B + s A < s z + s A ↔ A + s B ∈ No ∧ B < s C → B + s A < s C + s A
41 35 40 imbi12d ⊢ z = C → bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ z ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → A + s B ∈ No ∧ B < s z → B + s A < s z + s A ↔ bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ C ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → A + s B ∈ No ∧ B < s C → B + s A < s C + s A
42 19 31 41 rspc3v ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → ∀ 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 → bday ⁡ A + bday ⁡ B ∪ bday ⁡ A + bday ⁡ C ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z → A + s B ∈ No ∧ B < s C → B + s A < s C + s A
43 6 1 5 42 syl3c ⊢ φ → A + s B ∈ No ∧ B < s C → B + s A < s C + s A