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

Theorem addscut 28029
Description: Demonstrate the cut properties of surreal addition. This gives us closure together with a pair of set-less-than relationships for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.)
Hypotheses
Ref Expression
addscut.1 (𝜑𝑋 No )
addscut.2 (𝜑𝑌 No )
Assertion
Ref Expression
addscut (𝜑 → ((𝑋 +s 𝑌) ∈ No ∧ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})))
Distinct variable groups:   𝑋,𝑝,𝑙   𝑋,𝑞,𝑚   𝑤,𝑋,𝑟   𝑡,𝑋,𝑠   𝑌,𝑝,𝑙   𝑌,𝑞,𝑚   𝑤,𝑌,𝑟   𝑡,𝑌,𝑠
Allowed substitution hints:   𝜑(𝑤,𝑡,𝑚,𝑠,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem addscut
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addscut.1 . . 3 (𝜑𝑋 No )
2 addscut.2 . . 3 (𝜑𝑌 No )
31, 2addscutlem 28028 . 2 (𝜑 → ((𝑋 +s 𝑌) ∈ No ∧ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑌)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s )})))
4 biid 261 . . 3 ((𝑋 +s 𝑌) ∈ No ↔ (𝑋 +s 𝑌) ∈ No )
5 oveq1 7455 . . . . . . . . 9 (𝑙 = 𝑏 → (𝑙 +s 𝑌) = (𝑏 +s 𝑌))
65eqeq2d 2751 . . . . . . . 8 (𝑙 = 𝑏 → (𝑝 = (𝑙 +s 𝑌) ↔ 𝑝 = (𝑏 +s 𝑌)))
76cbvrexvw 3244 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑏 ∈ ( L ‘𝑋)𝑝 = (𝑏 +s 𝑌))
8 eqeq1 2744 . . . . . . . 8 (𝑝 = 𝑎 → (𝑝 = (𝑏 +s 𝑌) ↔ 𝑎 = (𝑏 +s 𝑌)))
98rexbidv 3185 . . . . . . 7 (𝑝 = 𝑎 → (∃𝑏 ∈ ( L ‘𝑋)𝑝 = (𝑏 +s 𝑌) ↔ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑌)))
107, 9bitrid 283 . . . . . 6 (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑌)))
1110cbvabv 2815 . . . . 5 {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} = {𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑌)}
12 oveq2 7456 . . . . . . . . 9 (𝑚 = 𝑑 → (𝑋 +s 𝑚) = (𝑋 +s 𝑑))
1312eqeq2d 2751 . . . . . . . 8 (𝑚 = 𝑑 → (𝑞 = (𝑋 +s 𝑚) ↔ 𝑞 = (𝑋 +s 𝑑)))
1413cbvrexvw 3244 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑑 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑑))
15 eqeq1 2744 . . . . . . . 8 (𝑞 = 𝑐 → (𝑞 = (𝑋 +s 𝑑) ↔ 𝑐 = (𝑋 +s 𝑑)))
1615rexbidv 3185 . . . . . . 7 (𝑞 = 𝑐 → (∃𝑑 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑑) ↔ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)))
1714, 16bitrid 283 . . . . . 6 (𝑞 = 𝑐 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)))
1817cbvabv 2815 . . . . 5 {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} = {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)}
1911, 18uneq12i 4189 . . . 4 ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) = ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑌)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)})
2019breq1i 5173 . . 3 (({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s {(𝑋 +s 𝑌)} ↔ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑌)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑌)})
21 oveq1 7455 . . . . . . . . 9 (𝑟 = 𝑓 → (𝑟 +s 𝑌) = (𝑓 +s 𝑌))
2221eqeq2d 2751 . . . . . . . 8 (𝑟 = 𝑓 → (𝑤 = (𝑟 +s 𝑌) ↔ 𝑤 = (𝑓 +s 𝑌)))
2322cbvrexvw 3244 . . . . . . 7 (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑓 ∈ ( R ‘𝑋)𝑤 = (𝑓 +s 𝑌))
24 eqeq1 2744 . . . . . . . 8 (𝑤 = 𝑒 → (𝑤 = (𝑓 +s 𝑌) ↔ 𝑒 = (𝑓 +s 𝑌)))
2524rexbidv 3185 . . . . . . 7 (𝑤 = 𝑒 → (∃𝑓 ∈ ( R ‘𝑋)𝑤 = (𝑓 +s 𝑌) ↔ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)))
2623, 25bitrid 283 . . . . . 6 (𝑤 = 𝑒 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)))
2726cbvabv 2815 . . . . 5 {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} = {𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)}
28 oveq2 7456 . . . . . . . . 9 (𝑠 = → (𝑋 +s 𝑠) = (𝑋 +s ))
2928eqeq2d 2751 . . . . . . . 8 (𝑠 = → (𝑡 = (𝑋 +s 𝑠) ↔ 𝑡 = (𝑋 +s )))
3029cbvrexvw 3244 . . . . . . 7 (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃ ∈ ( R ‘𝑌)𝑡 = (𝑋 +s ))
31 eqeq1 2744 . . . . . . . 8 (𝑡 = 𝑔 → (𝑡 = (𝑋 +s ) ↔ 𝑔 = (𝑋 +s )))
3231rexbidv 3185 . . . . . . 7 (𝑡 = 𝑔 → (∃ ∈ ( R ‘𝑌)𝑡 = (𝑋 +s ) ↔ ∃ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s )))
3330, 32bitrid 283 . . . . . 6 (𝑡 = 𝑔 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s )))
3433cbvabv 2815 . . . . 5 {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} = {𝑔 ∣ ∃ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s )}
3527, 34uneq12i 4189 . . . 4 ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) = ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s )})
3635breq2i 5174 . . 3 ({(𝑋 +s 𝑌)} <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s )}))
374, 20, 363anbi123i 1155 . 2 (((𝑋 +s 𝑌) ∈ No ∧ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) ↔ ((𝑋 +s 𝑌) ∈ No ∧ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑌)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s )})))
383, 37sylibr 234 1 (𝜑 → ((𝑋 +s 𝑌) ∈ No ∧ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087   = wceq 1537  wcel 2108  {cab 2717  wrex 3076  cun 3974  {csn 4648   class class class wbr 5166  cfv 6573  (class class class)co 7448   No csur 27702   <<s csslt 27843   L cleft 27902   R cright 27903   +s cadds 28010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-1o 8522  df-2o 8523  df-nadd 8722  df-no 27705  df-slt 27706  df-bday 27707  df-sslt 27844  df-scut 27846  df-0s 27887  df-made 27904  df-old 27905  df-left 27907  df-right 27908  df-norec2 28000  df-adds 28011
This theorem is referenced by:  addscut2  28030  addscld  28031  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055
  Copyright terms: Public domain W3C validator