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

Definition df-scut 27632
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. Definition from [Gonshor] p. 7. (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 27631 . 2 class |s
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 csur 27489 . . . 4 class No
54cpw 4594 . . 3 class 𝒫 No
6 csslt 27629 . . . 4 class <<s
72cv 1532 . . . . 5 class 𝑎
87csn 4620 . . . 4 class {𝑎}
96, 8cima 5669 . . 3 class ( <<s “ {𝑎})
10 vx . . . . . . 7 setvar 𝑥
1110cv 1532 . . . . . 6 class 𝑥
12 cbday 27491 . . . . . 6 class bday
1311, 12cfv 6533 . . . . 5 class ( bday 𝑥)
14 vy . . . . . . . . . . . 12 setvar 𝑦
1514cv 1532 . . . . . . . . . . 11 class 𝑦
1615csn 4620 . . . . . . . . . 10 class {𝑦}
177, 16, 6wbr 5138 . . . . . . . . 9 wff 𝑎 <<s {𝑦}
183cv 1532 . . . . . . . . . 10 class 𝑏
1916, 18, 6wbr 5138 . . . . . . . . 9 wff {𝑦} <<s 𝑏
2017, 19wa 395 . . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
2120, 14, 4crab 3424 . . . . . . 7 class {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
2212, 21cima 5669 . . . . . 6 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2322cint 4940 . . . . 5 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2413, 23wceq 1533 . . . 4 wff ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2524, 10, 21crio 7356 . . 3 class (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
262, 3, 5, 9, 25cmpo 7403 . 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
271, 26wceq 1533 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  27649  dmscut  27660  scutf  27661
  Copyright terms: Public domain W3C validator