Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-scut Structured version   Visualization version   GIF version

Definition df-scut 32230
Description: Define the cut operator on surreal numbers. This operator, which Conway takes as the primitive operator over surreals, picks the surreal lying between two sets of surreals of minimal birthday. (Contributed by Scott Fenton, 7-Dec-2021.)
Assertion
Ref Expression
df-scut |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
Distinct variable group:   𝑎,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-scut
StepHypRef Expression
1 cscut 32229 . 2 class |s
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 csur 32124 . . . 4 class No
54cpw 4295 . . 3 class 𝒫 No
6 csslt 32227 . . . 4 class <<s
72cv 1629 . . . . 5 class 𝑎
87csn 4314 . . . 4 class {𝑎}
96, 8cima 5252 . . 3 class ( <<s “ {𝑎})
10 vx . . . . . . 7 setvar 𝑥
1110cv 1629 . . . . . 6 class 𝑥
12 cbday 32126 . . . . . 6 class bday
1311, 12cfv 6031 . . . . 5 class ( bday 𝑥)
14 vy . . . . . . . . . . . 12 setvar 𝑦
1514cv 1629 . . . . . . . . . . 11 class 𝑦
1615csn 4314 . . . . . . . . . 10 class {𝑦}
177, 16, 6wbr 4784 . . . . . . . . 9 wff 𝑎 <<s {𝑦}
183cv 1629 . . . . . . . . . 10 class 𝑏
1916, 18, 6wbr 4784 . . . . . . . . 9 wff {𝑦} <<s 𝑏
2017, 19wa 382 . . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
2120, 14, 4crab 3064 . . . . . . 7 class {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
2212, 21cima 5252 . . . . . 6 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2322cint 4609 . . . . 5 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2413, 23wceq 1630 . . . 4 wff ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2524, 10, 21crio 6752 . . 3 class (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
262, 3, 5, 9, 25cmpt2 6794 . 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
271, 26wceq 1630 1 wff |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
Colors of variables: wff setvar class
This definition is referenced by:  scutval  32242  dmscut  32249  scutf  32250
  Copyright terms: Public domain W3C validator