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 27846
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 27845 . 2 class |s
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 csur 27702 . . . 4 class No
54cpw 4622 . . 3 class 𝒫 No
6 csslt 27843 . . . 4 class <<s
72cv 1536 . . . . 5 class 𝑎
87csn 4648 . . . 4 class {𝑎}
96, 8cima 5703 . . 3 class ( <<s “ {𝑎})
10 vx . . . . . . 7 setvar 𝑥
1110cv 1536 . . . . . 6 class 𝑥
12 cbday 27704 . . . . . 6 class bday
1311, 12cfv 6573 . . . . 5 class ( bday 𝑥)
14 vy . . . . . . . . . . . 12 setvar 𝑦
1514cv 1536 . . . . . . . . . . 11 class 𝑦
1615csn 4648 . . . . . . . . . 10 class {𝑦}
177, 16, 6wbr 5166 . . . . . . . . 9 wff 𝑎 <<s {𝑦}
183cv 1536 . . . . . . . . . 10 class 𝑏
1916, 18, 6wbr 5166 . . . . . . . . 9 wff {𝑦} <<s 𝑏
2017, 19wa 395 . . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
2120, 14, 4crab 3443 . . . . . . 7 class {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
2212, 21cima 5703 . . . . . 6 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2322cint 4970 . . . . 5 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2413, 23wceq 1537 . . . 4 wff ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2524, 10, 21crio 7403 . . 3 class (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
262, 3, 5, 9, 25cmpo 7450 . 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
271, 26wceq 1537 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  27863  dmscut  27874  scutf  27875
  Copyright terms: Public domain W3C validator