Metamath Proof Explorer

Theorem addsproplem6

Description: Lemma for surreal addition properties. Finally, we show the second half of the induction hypothesis when Y and Z are the same age. (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
addsproplem6.6 ⊢ φ → bday ⁡ Y = bday ⁡ Z
Assertion addsproplem6 ⊢ φ → 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 addsproplem6.6 ⊢ φ → bday ⁡ Y = bday ⁡ Z
7 nodense ⊢ Y ∈ No ∧ Z ∈ No ∧ bday ⁡ Y = bday ⁡ Z ∧ Y < s Z → ∃ m ∈ No bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z
8 3 4 6 5 7 syl22anc ⊢ φ → ∃ m ∈ No bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z
9 1 2 3 addsproplem3 ⊢ φ → 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
10 9 simp1d ⊢ φ → X + s Y ∈ No
11 10 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Y ∈ No
12 1 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s 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
13 2 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X ∈ No
14 simprl ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ No
15 unidm ⊢ bday ⁡ X + bday ⁡ m ∪ bday ⁡ X + bday ⁡ m = bday ⁡ X + bday ⁡ m
16 simprr1 ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → bday ⁡ m ∈ bday ⁡ Y
17 bdayelon ⊢ bday ⁡ m ∈ On
18 bdayelon ⊢ bday ⁡ Y ∈ On
19 bdayelon ⊢ bday ⁡ X ∈ On
20 naddel2 ⊢ bday ⁡ m ∈ On ∧ bday ⁡ Y ∈ On ∧ bday ⁡ X ∈ On → bday ⁡ m ∈ bday ⁡ Y ↔ bday ⁡ X + bday ⁡ m ∈ bday ⁡ X + bday ⁡ Y
21 17 18 19 20 mp3an ⊢ bday ⁡ m ∈ bday ⁡ Y ↔ bday ⁡ X + bday ⁡ m ∈ bday ⁡ X + bday ⁡ Y
22 16 21 sylib ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → bday ⁡ X + bday ⁡ m ∈ bday ⁡ X + bday ⁡ Y
23 elun1 ⊢ bday ⁡ X + bday ⁡ m ∈ bday ⁡ X + bday ⁡ Y → bday ⁡ X + bday ⁡ m ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
24 22 23 syl ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → bday ⁡ X + bday ⁡ m ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
25 15 24 eqeltrid ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → bday ⁡ X + bday ⁡ m ∪ bday ⁡ X + bday ⁡ m ∈ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z
26 12 13 14 14 25 addsproplem1 ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m ∈ No ∧ m < s m → m + s X < s m + s X
27 26 simpld ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m ∈ No
28 uncom ⊢ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ X + bday ⁡ Z = bday ⁡ X + bday ⁡ Z ∪ bday ⁡ X + bday ⁡ Y
29 28 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
30 29 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
31 30 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
32 31 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
33 1 32 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
34 33 2 4 addsproplem3 ⊢ φ → X + s Z ∈ No ∧ a | ∃ b ∈ L ⁡ X a = b + s Z ∪ c | ∃ d ∈ L ⁡ Z c = X + s d ≪ s X + s Z ∧ X + s Z ≪ s e | ∃ f ∈ R ⁡ X e = f + s Z ∪ g | ∃ h ∈ R ⁡ Z g = X + s h
35 34 simp1d ⊢ φ → X + s Z ∈ No
36 35 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Z ∈ No
37 9 simp3d ⊢ φ → X + s Y ≪ s e | ∃ f ∈ R ⁡ X e = f + s Y ∪ g | ∃ h ∈ R ⁡ Y g = X + s h
38 37 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Y ≪ s e | ∃ f ∈ R ⁡ X e = f + s Y ∪ g | ∃ h ∈ R ⁡ Y g = X + s h
39 ovex ⊢ X + s Y ∈ V
40 39 snid ⊢ X + s Y ∈ X + s Y
41 40 a1i ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Y ∈ X + s Y
42 oldbday ⊢ bday ⁡ Y ∈ On ∧ m ∈ No → m ∈ Old ⁡ bday ⁡ Y ↔ bday ⁡ m ∈ bday ⁡ Y
43 18 14 42 sylancr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ Old ⁡ bday ⁡ Y ↔ bday ⁡ m ∈ bday ⁡ Y
44 16 43 mpbird ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ Old ⁡ bday ⁡ Y
45 simprr2 ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → Y < s m
46 breq2 ⊢ a = m → Y < s a ↔ Y < s m
47 rightval ⊢ R ⁡ Y = a ∈ Old ⁡ bday ⁡ Y | Y < s a
48 46 47 elrab2 ⊢ m ∈ R ⁡ Y ↔ m ∈ Old ⁡ bday ⁡ Y ∧ Y < s m
49 44 45 48 sylanbrc ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ R ⁡ Y
50 eqid ⊢ X + s m = X + s m
51 oveq2 ⊢ h = m → X + s h = X + s m
52 51 rspceeqv ⊢ m ∈ R ⁡ Y ∧ X + s m = X + s m → ∃ h ∈ R ⁡ Y X + s m = X + s h
53 49 50 52 sylancl ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → ∃ h ∈ R ⁡ Y X + s m = X + s h
54 ovex ⊢ X + s m ∈ V
55 eqeq1 ⊢ g = X + s m → g = X + s h ↔ X + s m = X + s h
56 55 rexbidv ⊢ g = X + s m → ∃ h ∈ R ⁡ Y g = X + s h ↔ ∃ h ∈ R ⁡ Y X + s m = X + s h
57 54 56 elab ⊢ X + s m ∈ g | ∃ h ∈ R ⁡ Y g = X + s h ↔ ∃ h ∈ R ⁡ Y X + s m = X + s h
58 53 57 sylibr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m ∈ g | ∃ h ∈ R ⁡ Y g = X + s h
59 elun2 ⊢ X + s m ∈ g | ∃ h ∈ R ⁡ Y g = X + s h → X + s m ∈ e | ∃ f ∈ R ⁡ X e = f + s Y ∪ g | ∃ h ∈ R ⁡ Y g = X + s h
60 58 59 syl ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m ∈ e | ∃ f ∈ R ⁡ X e = f + s Y ∪ g | ∃ h ∈ R ⁡ Y g = X + s h
61 38 41 60 ssltsepcd ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Y < s X + s m
62 33 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → ∀ 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
63 4 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → Z ∈ No
64 62 13 63 addsproplem3 ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Z ∈ No ∧ a | ∃ b ∈ L ⁡ X a = b + s Z ∪ c | ∃ d ∈ L ⁡ Z c = X + s d ≪ s X + s Z ∧ X + s Z ≪ s e | ∃ f ∈ R ⁡ X e = f + s Z ∪ g | ∃ h ∈ R ⁡ Z g = X + s h
65 64 simp2d ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → a | ∃ b ∈ L ⁡ X a = b + s Z ∪ c | ∃ d ∈ L ⁡ Z c = X + s d ≪ s X + s Z
66 6 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → bday ⁡ Y = bday ⁡ Z
67 16 66 eleqtrd ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → bday ⁡ m ∈ bday ⁡ Z
68 bdayelon ⊢ bday ⁡ Z ∈ On
69 oldbday ⊢ bday ⁡ Z ∈ On ∧ m ∈ No → m ∈ Old ⁡ bday ⁡ Z ↔ bday ⁡ m ∈ bday ⁡ Z
70 68 14 69 sylancr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ Old ⁡ bday ⁡ Z ↔ bday ⁡ m ∈ bday ⁡ Z
71 67 70 mpbird ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ Old ⁡ bday ⁡ Z
72 simprr3 ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m < s Z
73 breq1 ⊢ a = m → a < s Z ↔ m < s Z
74 leftval ⊢ L ⁡ Z = a ∈ Old ⁡ bday ⁡ Z | a < s Z
75 73 74 elrab2 ⊢ m ∈ L ⁡ Z ↔ m ∈ Old ⁡ bday ⁡ Z ∧ m < s Z
76 71 72 75 sylanbrc ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ L ⁡ Z
77 oveq2 ⊢ d = m → X + s d = X + s m
78 77 rspceeqv ⊢ m ∈ L ⁡ Z ∧ X + s m = X + s m → ∃ d ∈ L ⁡ Z X + s m = X + s d
79 76 50 78 sylancl ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → ∃ d ∈ L ⁡ Z X + s m = X + s d
80 eqeq1 ⊢ c = X + s m → c = X + s d ↔ X + s m = X + s d
81 80 rexbidv ⊢ c = X + s m → ∃ d ∈ L ⁡ Z c = X + s d ↔ ∃ d ∈ L ⁡ Z X + s m = X + s d
82 54 81 elab ⊢ X + s m ∈ c | ∃ d ∈ L ⁡ Z c = X + s d ↔ ∃ d ∈ L ⁡ Z X + s m = X + s d
83 79 82 sylibr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m ∈ c | ∃ d ∈ L ⁡ Z c = X + s d
84 elun2 ⊢ X + s m ∈ c | ∃ d ∈ L ⁡ Z c = X + s d → X + s m ∈ a | ∃ b ∈ L ⁡ X a = b + s Z ∪ c | ∃ d ∈ L ⁡ Z c = X + s d
85 83 84 syl ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m ∈ a | ∃ b ∈ L ⁡ X a = b + s Z ∪ c | ∃ d ∈ L ⁡ Z c = X + s d
86 ovex ⊢ X + s Z ∈ V
87 86 snid ⊢ X + s Z ∈ X + s Z
88 87 a1i ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Z ∈ X + s Z
89 65 85 88 ssltsepcd ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m < s X + s Z
90 11 27 36 61 89 slttrd ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Y < s X + s Z
91 8 90 rexlimddv ⊢ φ → X + s Y < s X + s Z
92 3 2 addscomd ⊢ φ → Y + s X = X + s Y
93 4 2 addscomd ⊢ φ → Z + s X = X + s Z
94 91 92 93 3brtr4d ⊢ φ → Y + s X < s Z + s X