MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addsproplem1 Structured version   Visualization version   GIF version

Theorem addsproplem1 27899
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 8413 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.)
Hypotheses
Ref Expression
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
Ref Expression
addsproplem1 (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴))))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑦,𝐵,𝑧   𝑧,𝐶   𝑥,𝑋,𝑦,𝑧   𝑥,𝑌,𝑦,𝑧   𝑥,𝑍,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝐵(𝑥)   𝐶(𝑥,𝑦)

Proof of Theorem addsproplem1
StepHypRef Expression
1 addsproplem1.2 . . 3 (𝜑𝐴 No )
2 addsproplem1.3 . . 3 (𝜑𝐵 No )
3 addsproplem1.4 . . 3 (𝜑𝐶 No )
41, 2, 33jca 1125 . 2 (𝜑 → (𝐴 No 𝐵 No 𝐶 No ))
5 addsproplem.1 . 2 (𝜑 → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
6 addsproplem1.5 . 2 (𝜑 → ((( bday 𝐴) +no ( bday 𝐵)) ∪ (( bday 𝐴) +no ( bday 𝐶))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
7 fveq2 6890 . . . . . . 7 (𝑥 = 𝐴 → ( bday 𝑥) = ( bday 𝐴))
87oveq1d 7428 . . . . . 6 (𝑥 = 𝐴 → (( bday 𝑥) +no ( bday 𝑦)) = (( bday 𝐴) +no ( bday 𝑦)))
97oveq1d 7428 . . . . . 6 (𝑥 = 𝐴 → (( bday 𝑥) +no ( bday 𝑧)) = (( bday 𝐴) +no ( bday 𝑧)))
108, 9uneq12d 4158 . . . . 5 (𝑥 = 𝐴 → ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) = ((( bday 𝐴) +no ( bday 𝑦)) ∪ (( bday 𝐴) +no ( bday 𝑧))))
1110eleq1d 2810 . . . 4 (𝑥 = 𝐴 → (((( 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 7420 . . . . . 6 (𝑥 = 𝐴 → (𝑥 +s 𝑦) = (𝐴 +s 𝑦))
1312eleq1d 2810 . . . . 5 (𝑥 = 𝐴 → ((𝑥 +s 𝑦) ∈ No ↔ (𝐴 +s 𝑦) ∈ No ))
14 oveq2 7421 . . . . . . 7 (𝑥 = 𝐴 → (𝑦 +s 𝑥) = (𝑦 +s 𝐴))
15 oveq2 7421 . . . . . . 7 (𝑥 = 𝐴 → (𝑧 +s 𝑥) = (𝑧 +s 𝐴))
1614, 15breq12d 5157 . . . . . 6 (𝑥 = 𝐴 → ((𝑦 +s 𝑥) <s (𝑧 +s 𝑥) ↔ (𝑦 +s 𝐴) <s (𝑧 +s 𝐴)))
1716imbi2d 339 . . . . 5 (𝑥 = 𝐴 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)) ↔ (𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴))))
1813, 17anbi12d 630 . . . 4 (𝑥 = 𝐴 → (((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))) ↔ ((𝐴 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴)))))
1911, 18imbi12d 343 . . 3 (𝑥 = 𝐴 → ((((( 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 6890 . . . . . . 7 (𝑦 = 𝐵 → ( bday 𝑦) = ( bday 𝐵))
2120oveq2d 7429 . . . . . 6 (𝑦 = 𝐵 → (( bday 𝐴) +no ( bday 𝑦)) = (( bday 𝐴) +no ( bday 𝐵)))
2221uneq1d 4156 . . . . 5 (𝑦 = 𝐵 → ((( bday 𝐴) +no ( bday 𝑦)) ∪ (( bday 𝐴) +no ( bday 𝑧))) = ((( bday 𝐴) +no ( bday 𝐵)) ∪ (( bday 𝐴) +no ( bday 𝑧))))
2322eleq1d 2810 . . . 4 (𝑦 = 𝐵 → (((( 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 7421 . . . . . 6 (𝑦 = 𝐵 → (𝐴 +s 𝑦) = (𝐴 +s 𝐵))
2524eleq1d 2810 . . . . 5 (𝑦 = 𝐵 → ((𝐴 +s 𝑦) ∈ No ↔ (𝐴 +s 𝐵) ∈ No ))
26 breq1 5147 . . . . . 6 (𝑦 = 𝐵 → (𝑦 <s 𝑧𝐵 <s 𝑧))
27 oveq1 7420 . . . . . . 7 (𝑦 = 𝐵 → (𝑦 +s 𝐴) = (𝐵 +s 𝐴))
2827breq1d 5154 . . . . . 6 (𝑦 = 𝐵 → ((𝑦 +s 𝐴) <s (𝑧 +s 𝐴) ↔ (𝐵 +s 𝐴) <s (𝑧 +s 𝐴)))
2926, 28imbi12d 343 . . . . 5 (𝑦 = 𝐵 → ((𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴)) ↔ (𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴))))
3025, 29anbi12d 630 . . . 4 (𝑦 = 𝐵 → (((𝐴 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝐴) <s (𝑧 +s 𝐴))) ↔ ((𝐴 +s 𝐵) ∈ No ∧ (𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴)))))
3123, 30imbi12d 343 . . 3 (𝑦 = 𝐵 → ((((( 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 6890 . . . . . . 7 (𝑧 = 𝐶 → ( bday 𝑧) = ( bday 𝐶))
3332oveq2d 7429 . . . . . 6 (𝑧 = 𝐶 → (( bday 𝐴) +no ( bday 𝑧)) = (( bday 𝐴) +no ( bday 𝐶)))
3433uneq2d 4157 . . . . 5 (𝑧 = 𝐶 → ((( bday 𝐴) +no ( bday 𝐵)) ∪ (( bday 𝐴) +no ( bday 𝑧))) = ((( bday 𝐴) +no ( bday 𝐵)) ∪ (( bday 𝐴) +no ( bday 𝐶))))
3534eleq1d 2810 . . . 4 (𝑧 = 𝐶 → (((( 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 5148 . . . . . 6 (𝑧 = 𝐶 → (𝐵 <s 𝑧𝐵 <s 𝐶))
37 oveq1 7420 . . . . . . 7 (𝑧 = 𝐶 → (𝑧 +s 𝐴) = (𝐶 +s 𝐴))
3837breq2d 5156 . . . . . 6 (𝑧 = 𝐶 → ((𝐵 +s 𝐴) <s (𝑧 +s 𝐴) ↔ (𝐵 +s 𝐴) <s (𝐶 +s 𝐴)))
3936, 38imbi12d 343 . . . . 5 (𝑧 = 𝐶 → ((𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴)) ↔ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴))))
4039anbi2d 628 . . . 4 (𝑧 = 𝐶 → (((𝐴 +s 𝐵) ∈ No ∧ (𝐵 <s 𝑧 → (𝐵 +s 𝐴) <s (𝑧 +s 𝐴))) ↔ ((𝐴 +s 𝐵) ∈ No ∧ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴)))))
4135, 40imbi12d 343 . . 3 (𝑧 = 𝐶 → ((((( 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 𝐴))))))
4219, 31, 41rspc3v 3619 . 2 ((𝐴 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 𝐴))))))
434, 5, 6, 42syl3c 66 1 (𝜑 → ((𝐴 +s 𝐵) ∈ No ∧ (𝐵 <s 𝐶 → (𝐵 +s 𝐴) <s (𝐶 +s 𝐴))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3051  cun 3939   class class class wbr 5144  cfv 6543  (class class class)co 7413   +no cnadd 8679   No csur 27586   <s cslt 27587   bday cbday 27588   +s cadds 27889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3052  df-rab 3420  df-v 3465  df-dif 3944  df-un 3946  df-ss 3958  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5145  df-iota 6495  df-fv 6551  df-ov 7416
This theorem is referenced by:  addsproplem2  27900  addsproplem6  27904
  Copyright terms: Public domain W3C validator