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 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
addsproplem1.2 ⊢ ( 𝜑 → 𝐴 ∈ No )
addsproplem1.3 ⊢ ( 𝜑 → 𝐵 ∈ No )
addsproplem1.4 ⊢ ( 𝜑 → 𝐶 ∈ No )
addsproplem1.5 ⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐶 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
Assertion addsproplem1 ( 𝜑 → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝐶 → ( 𝐵 +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 addsproplem1.2 ⊢ ( 𝜑 → 𝐴 ∈ No )
3 addsproplem1.3 ⊢ ( 𝜑 → 𝐵 ∈ No )
4 addsproplem1.4 ⊢ ( 𝜑 → 𝐶 ∈ No )
5 addsproplem1.5 ⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐶 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
6 2 3 4 3jca ⊢ ( 𝜑 → ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) )
7 fveq2 ⊢ ( 𝑥 = 𝐴 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝐴 ) )
8 7 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) )
9 7 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) )
10 8 9 uneq12d ⊢ ( 𝑥 = 𝐴 → ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) )
11 10 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ↔ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ) )
12 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 +s 𝑦 ) = ( 𝐴 +s 𝑦 ) )
13 12 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 +s 𝑦 ) ∈ No ↔ ( 𝐴 +s 𝑦 ) ∈ No ) )
14 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 +s 𝑥 ) = ( 𝑦 +s 𝐴 ) )
15 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑧 +s 𝑥 ) = ( 𝑧 +s 𝐴 ) )
16 14 15 breq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ↔ ( 𝑦 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) )
17 16 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ↔ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) )
18 13 17 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ↔ ( ( 𝐴 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) ) )
19 11 18 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) ↔ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝐴 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) ) ) )
20 fveq2 ⊢ ( 𝑦 = 𝐵 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝐵 ) )
21 20 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
22 21 uneq1d ⊢ ( 𝑦 = 𝐵 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) )
23 22 eleq1d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ↔ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ) )
24 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 +s 𝑦 ) = ( 𝐴 +s 𝐵 ) )
25 24 eleq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 +s 𝑦 ) ∈ No ↔ ( 𝐴 +s 𝐵 ) ∈ No ) )
26 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 <s 𝑧 ↔ 𝐵 <s 𝑧 ) )
27 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 +s 𝐴 ) = ( 𝐵 +s 𝐴 ) )
28 27 breq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ↔ ( 𝐵 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) )
29 26 28 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ↔ ( 𝐵 <s 𝑧 → ( 𝐵 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) )
30 25 29 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) ↔ ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝑧 → ( 𝐵 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) ) )
31 23 30 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝐴 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) ) ↔ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝑧 → ( 𝐵 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) ) ) )
32 fveq2 ⊢ ( 𝑧 = 𝐶 → ( bday ‘ 𝑧 ) = ( bday ‘ 𝐶 ) )
33 32 oveq2d ⊢ ( 𝑧 = 𝐶 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐶 ) ) )
34 33 uneq2d ⊢ ( 𝑧 = 𝐶 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐶 ) ) ) )
35 34 eleq1d ⊢ ( 𝑧 = 𝐶 → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ↔ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐶 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ) )
36 breq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐵 <s 𝑧 ↔ 𝐵 <s 𝐶 ) )
37 oveq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 +s 𝐴 ) = ( 𝐶 +s 𝐴 ) )
38 37 breq2d ⊢ ( 𝑧 = 𝐶 → ( ( 𝐵 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ↔ ( 𝐵 +s 𝐴 ) <s ( 𝐶 +s 𝐴 ) ) )
39 36 38 imbi12d ⊢ ( 𝑧 = 𝐶 → ( ( 𝐵 <s 𝑧 → ( 𝐵 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ↔ ( 𝐵 <s 𝐶 → ( 𝐵 +s 𝐴 ) <s ( 𝐶 +s 𝐴 ) ) ) )
40 39 anbi2d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝑧 → ( 𝐵 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) ↔ ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝐶 → ( 𝐵 +s 𝐴 ) <s ( 𝐶 +s 𝐴 ) ) ) ) )
41 35 40 imbi12d ⊢ ( 𝑧 = 𝐶 → ( ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝑧 → ( 𝐵 +s 𝐴 ) <s ( 𝑧 +s 𝐴 ) ) ) ) ↔ ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐶 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝐶 → ( 𝐵 +s 𝐴 ) <s ( 𝐶 +s 𝐴 ) ) ) ) ) )
42 19 31 41 rspc3v ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) → ( ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐶 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝐶 → ( 𝐵 +s 𝐴 ) <s ( 𝐶 +s 𝐴 ) ) ) ) ) )
43 6 1 5 42 syl3c ⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) ∈ No ∧ ( 𝐵 <s 𝐶 → ( 𝐵 +s 𝐴 ) <s ( 𝐶 +s 𝐴 ) ) ) )