Metamath Proof Explorer

Theorem addsproplem7

Description: Lemma for surreal addition properties. Putting together the three previous lemmas, we now show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsproplem.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
addspropord.2 ⊢ ( 𝜑 → 𝑋 ∈ No )
addspropord.3 ⊢ ( 𝜑 → 𝑌 ∈ No )
addspropord.4 ⊢ ( 𝜑 → 𝑍 ∈ No )
addspropord.5 ⊢ ( 𝜑 → 𝑌 <s 𝑍 )
Assertion addsproplem7 ( 𝜑 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) )

Proof

Step Hyp Ref Expression
1 addsproplem.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
2 addspropord.2 ⊢ ( 𝜑 → 𝑋 ∈ No )
3 addspropord.3 ⊢ ( 𝜑 → 𝑌 ∈ No )
4 addspropord.4 ⊢ ( 𝜑 → 𝑍 ∈ No )
5 addspropord.5 ⊢ ( 𝜑 → 𝑌 <s 𝑍 )
6 bdayelon ⊢ ( bday ‘ 𝑌 ) ∈ On
7 fvex ⊢ ( bday ‘ 𝑌 ) ∈ V
8 7 elon ⊢ ( ( bday ‘ 𝑌 ) ∈ On ↔ Ord ( bday ‘ 𝑌 ) )
9 6 8 mpbi ⊢ Ord ( bday ‘ 𝑌 )
10 bdayelon ⊢ ( bday ‘ 𝑍 ) ∈ On
11 fvex ⊢ ( bday ‘ 𝑍 ) ∈ V
12 11 elon ⊢ ( ( bday ‘ 𝑍 ) ∈ On ↔ Ord ( bday ‘ 𝑍 ) )
13 10 12 mpbi ⊢ Ord ( bday ‘ 𝑍 )
14 ordtri3or ⊢ ( ( Ord ( bday ‘ 𝑌 ) ∧ Ord ( bday ‘ 𝑍 ) ) → ( ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ∨ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ∨ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) )
15 9 13 14 mp2an ⊢ ( ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ∨ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ∨ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) )
16 simpl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) → 𝜑 )
17 16 1 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
18 16 2 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) → 𝑋 ∈ No )
19 16 3 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) → 𝑌 ∈ No )
20 16 4 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) → 𝑍 ∈ No )
21 16 5 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) → 𝑌 <s 𝑍 )
22 simpr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) → ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) )
23 17 18 19 20 21 22 addsproplem4 ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) )
24 23 ex ⊢ ( 𝜑 → ( ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) )
25 simpl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ) → 𝜑 )
26 25 1 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
27 25 2 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ) → 𝑋 ∈ No )
28 25 3 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ) → 𝑌 ∈ No )
29 25 4 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ) → 𝑍 ∈ No )
30 25 5 syl ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ) → 𝑌 <s 𝑍 )
31 simpr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ) → ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) )
32 26 27 28 29 30 31 addsproplem6 ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ) → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) )
33 32 ex ⊢ ( 𝜑 → ( ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) )
34 1 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
35 2 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) → 𝑋 ∈ No )
36 3 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) → 𝑌 ∈ No )
37 4 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) → 𝑍 ∈ No )
38 5 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) → 𝑌 <s 𝑍 )
39 simpr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) → ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) )
40 34 35 36 37 38 39 addsproplem5 ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) )
41 40 ex ⊢ ( 𝜑 → ( ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) )
42 24 33 41 3jaod ⊢ ( 𝜑 → ( ( ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ∨ ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ∨ ( bday ‘ 𝑍 ) ∈ ( bday ‘ 𝑌 ) ) → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) )
43 15 42 mpi ⊢ ( 𝜑 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) )