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 27703
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 27702 . 2 class |s
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 csur 27560 . . . 4 class No
54cpw 4598 . . 3 class 𝒫 No
6 csslt 27700 . . . 4 class <<s
72cv 1533 . . . . 5 class 𝑎
87csn 4624 . . . 4 class {𝑎}
96, 8cima 5675 . . 3 class ( <<s “ {𝑎})
10 vx . . . . . . 7 setvar 𝑥
1110cv 1533 . . . . . 6 class 𝑥
12 cbday 27562 . . . . . 6 class bday
1311, 12cfv 6542 . . . . 5 class ( bday 𝑥)
14 vy . . . . . . . . . . . 12 setvar 𝑦
1514cv 1533 . . . . . . . . . . 11 class 𝑦
1615csn 4624 . . . . . . . . . 10 class {𝑦}
177, 16, 6wbr 5142 . . . . . . . . 9 wff 𝑎 <<s {𝑦}
183cv 1533 . . . . . . . . . 10 class 𝑏
1916, 18, 6wbr 5142 . . . . . . . . 9 wff {𝑦} <<s 𝑏
2017, 19wa 395 . . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
2120, 14, 4crab 3427 . . . . . . 7 class {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
2212, 21cima 5675 . . . . . 6 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2322cint 4944 . . . . 5 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2413, 23wceq 1534 . . . 4 wff ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2524, 10, 21crio 7369 . . 3 class (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
262, 3, 5, 9, 25cmpo 7416 . 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
271, 26wceq 1534 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  27720  dmscut  27731  scutf  27732
  Copyright terms: Public domain W3C validator