Definition df-scut 27843

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

Step	Hyp	Ref	Expression
1		cscut 27842	. 2 class |s
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		csur 27699	. . . 4 class No
5	4	cpw 4605	. . 3 class 𝒫 No
6		csslt 27840	. . . 4 class <<s
7	2	cv 1536	. . . . 5 class 𝑎
8	7	csn 4631	. . . 4 class {𝑎}
9	6, 8	cima 5692	. . 3 class ( <<s “ {𝑎})
10		vx	. . . . . . 7 setvar 𝑥
11	10	cv 1536	. . . . . 6 class 𝑥
12		cbday 27701	. . . . . 6 class bday
13	11, 12	cfv 6563	. . . . 5 class ( bday ‘𝑥)
14		vy	. . . . . . . . . . . 12 setvar 𝑦
15	14	cv 1536	. . . . . . . . . . 11 class 𝑦
16	15	csn 4631	. . . . . . . . . 10 class {𝑦}
17	7, 16, 6	wbr 5148	. . . . . . . . 9 wff 𝑎 <<s {𝑦}
18	3	cv 1536	. . . . . . . . . 10 class 𝑏
19	16, 18, 6	wbr 5148	. . . . . . . . 9 wff {𝑦} <<s 𝑏
20	17, 19	wa 395	. . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
21	20, 14, 4	crab 3433	. . . . . . 7 class {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
22	12, 21	cima 5692	. . . . . 6 class ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
23	22	cint 4951	. . . . 5 class ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
24	13, 23	wceq 1537	. . . 4 wff ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
25	24, 10, 21	crio 7387	. . 3 class (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
26	2, 3, 5, 9, 25	cmpo 7433	. 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
27	1, 26	wceq 1537	1 wff |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))

This definition is referenced by:  scutval  27860  dmscut  27871  scutf  27872