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 elright ⊢ m ∈ R ⁡ Y ↔ m ∈ Old ⁡ bday ⁡ Y ∧ Y < s m
47 44 45 46 sylanbrc ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ R ⁡ Y
48 eqid ⊢ X + s m = X + s m
49 oveq2 ⊢ h = m → X + s h = X + s m
50 49 rspceeqv ⊢ m ∈ R ⁡ Y ∧ X + s m = X + s m → ∃ h ∈ R ⁡ Y X + s m = X + s h
51 47 48 50 sylancl ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → ∃ h ∈ R ⁡ Y X + s m = X + s h
52 ovex ⊢ X + s m ∈ V
53 eqeq1 ⊢ g = X + s m → g = X + s h ↔ X + s m = X + s h
54 53 rexbidv ⊢ g = X + s m → ∃ h ∈ R ⁡ Y g = X + s h ↔ ∃ h ∈ R ⁡ Y X + s m = X + s h
55 52 54 elab ⊢ X + s m ∈ g | ∃ h ∈ R ⁡ Y g = X + s h ↔ ∃ h ∈ R ⁡ Y X + s m = X + s h
56 51 55 sylibr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m ∈ g | ∃ h ∈ R ⁡ Y g = X + s h
57 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
58 56 57 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
59 38 41 58 ssltsepcd ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Y < s X + s m
60 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
61 4 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → Z ∈ No
62 60 13 61 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
63 62 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
64 6 adantr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → bday ⁡ Y = bday ⁡ Z
65 16 64 eleqtrd ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → bday ⁡ m ∈ bday ⁡ Z
66 bdayelon ⊢ bday ⁡ Z ∈ On
67 oldbday ⊢ bday ⁡ Z ∈ On ∧ m ∈ No → m ∈ Old ⁡ bday ⁡ Z ↔ bday ⁡ m ∈ bday ⁡ Z
68 66 14 67 sylancr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ Old ⁡ bday ⁡ Z ↔ bday ⁡ m ∈ bday ⁡ Z
69 65 68 mpbird ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ Old ⁡ bday ⁡ Z
70 simprr3 ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m < s Z
71 elleft ⊢ m ∈ L ⁡ Z ↔ m ∈ Old ⁡ bday ⁡ Z ∧ m < s Z
72 69 70 71 sylanbrc ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → m ∈ L ⁡ Z
73 oveq2 ⊢ d = m → X + s d = X + s m
74 73 rspceeqv ⊢ m ∈ L ⁡ Z ∧ X + s m = X + s m → ∃ d ∈ L ⁡ Z X + s m = X + s d
75 72 48 74 sylancl ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → ∃ d ∈ L ⁡ Z X + s m = X + s d
76 eqeq1 ⊢ c = X + s m → c = X + s d ↔ X + s m = X + s d
77 76 rexbidv ⊢ c = X + s m → ∃ d ∈ L ⁡ Z c = X + s d ↔ ∃ d ∈ L ⁡ Z X + s m = X + s d
78 52 77 elab ⊢ X + s m ∈ c | ∃ d ∈ L ⁡ Z c = X + s d ↔ ∃ d ∈ L ⁡ Z X + s m = X + s d
79 75 78 sylibr ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m ∈ c | ∃ d ∈ L ⁡ Z c = X + s d
80 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
81 79 80 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
82 ovex ⊢ X + s Z ∈ V
83 82 snid ⊢ X + s Z ∈ X + s Z
84 83 a1i ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Z ∈ X + s Z
85 63 81 84 ssltsepcd ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s m < s X + s Z
86 11 27 36 59 85 slttrd ⊢ φ ∧ m ∈ No ∧ bday ⁡ m ∈ bday ⁡ Y ∧ Y < s m ∧ m < s Z → X + s Y < s X + s Z
87 8 86 rexlimddv ⊢ φ → X + s Y < s X + s Z
88 3 2 addscomd ⊢ φ → Y + s X = X + s Y
89 4 2 addscomd ⊢ φ → Z + s X = X + s Z
90 87 88 89 3brtr4d ⊢ φ → Y + s X < s Z + s X