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

Theorem dmscut 27856
Description: The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.)
Assertion
Ref Expression
dmscut dom |s = <<s

Proof of Theorem dmscut
Dummy variables 𝑎 𝑏 𝑐 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmoprab 7536 . 2 dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}
2 df-scut 27828 . . . 4 |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
3 df-mpo 7436 . . . 4 (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) = {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}
42, 3eqtri 2765 . . 3 |s = {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}
54dmeqi 5915 . 2 dom |s = dom {⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∣ ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}
6 df-sslt 27826 . . . . 5 <<s = {⟨𝑎, 𝑏⟩ ∣ (𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦)}
76relopabiv 5830 . . . 4 Rel <<s
8 19.42v 1953 . . . . . 6 (∃𝑐((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))) ↔ ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ ∃𝑐 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))))
9 ssltss1 27833 . . . . . . . . 9 (𝑎 <<s 𝑏𝑎 No )
10 velpw 4605 . . . . . . . . 9 (𝑎 ∈ 𝒫 No 𝑎 No )
119, 10sylibr 234 . . . . . . . 8 (𝑎 <<s 𝑏𝑎 ∈ 𝒫 No )
1211pm4.71ri 560 . . . . . . 7 (𝑎 <<s 𝑏 ↔ (𝑎 ∈ 𝒫 No 𝑎 <<s 𝑏))
13 vex 3484 . . . . . . . . . 10 𝑎 ∈ V
14 vex 3484 . . . . . . . . . 10 𝑏 ∈ V
1513, 14elimasn 6108 . . . . . . . . 9 (𝑏 ∈ ( <<s “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ <<s )
16 df-br 5144 . . . . . . . . 9 (𝑎 <<s 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ <<s )
1715, 16bitr4i 278 . . . . . . . 8 (𝑏 ∈ ( <<s “ {𝑎}) ↔ 𝑎 <<s 𝑏)
1817anbi2i 623 . . . . . . 7 ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ↔ (𝑎 ∈ 𝒫 No 𝑎 <<s 𝑏))
19 riotaex 7392 . . . . . . . . 9 (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})) ∈ V
2019isseti 3498 . . . . . . . 8 𝑐 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
2120biantru 529 . . . . . . 7 ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ↔ ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ ∃𝑐 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))))
2212, 18, 213bitr2i 299 . . . . . 6 (𝑎 <<s 𝑏 ↔ ((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ ∃𝑐 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))))
238, 22, 163bitr2ri 300 . . . . 5 (⟨𝑎, 𝑏⟩ ∈ <<s ↔ ∃𝑐((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))))
2423a1i 11 . . . 4 (⊤ → (⟨𝑎, 𝑏⟩ ∈ <<s ↔ ∃𝑐((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))))
257, 24opabbi2dv 5860 . . 3 (⊤ → <<s = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))})
2625mptru 1547 . 2 <<s = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐((𝑎 ∈ 𝒫 No 𝑏 ∈ ( <<s “ {𝑎})) ∧ 𝑐 = (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))}
271, 5, 263eqtr4i 2775 1 dom |s = <<s
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3a 1087   = wceq 1540  wtru 1541  wex 1779  wcel 2108  wral 3061  {crab 3436  wss 3951  𝒫 cpw 4600  {csn 4626  cop 4632   cint 4946   class class class wbr 5143  {copab 5205  dom cdm 5685  cima 5688  cfv 6561  crio 7387  {coprab 7432  cmpo 7433   No csur 27684   <s cslt 27685   bday cbday 27686   <<s csslt 27825   |s cscut 27827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-riota 7388  df-oprab 7435  df-mpo 7436  df-sslt 27826  df-scut 27828
This theorem is referenced by:  scutf  27857  madeval2  27892
  Copyright terms: Public domain W3C validator