Definition df-scut 33619

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 33618	. 2 class |s
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		csur 33484	. . . 4 class No
5	4	cpw 4488	. . 3 class 𝒫 No
6		csslt 33616	. . . 4 class <<s
7	2	cv 1541	. . . . 5 class 𝑎
8	7	csn 4516	. . . 4 class {𝑎}
9	6, 8	cima 5528	. . 3 class ( <<s “ {𝑎})
10		vx	. . . . . . 7 setvar 𝑥
11	10	cv 1541	. . . . . 6 class 𝑥
12		cbday 33486	. . . . . 6 class bday
13	11, 12	cfv 6339	. . . . 5 class ( bday ‘𝑥)
14		vy	. . . . . . . . . . . 12 setvar 𝑦
15	14	cv 1541	. . . . . . . . . . 11 class 𝑦
16	15	csn 4516	. . . . . . . . . 10 class {𝑦}
17	7, 16, 6	wbr 5030	. . . . . . . . 9 wff 𝑎 <<s {𝑦}
18	3	cv 1541	. . . . . . . . . 10 class 𝑏
19	16, 18, 6	wbr 5030	. . . . . . . . 9 wff {𝑦} <<s 𝑏
20	17, 19	wa 399	. . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
21	20, 14, 4	crab 3057	. . . . . . 7 class {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
22	12, 21	cima 5528	. . . . . 6 class ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
23	22	cint 4836	. . . . 5 class ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
24	13, 23	wceq 1542	. . . 4 wff ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
25	24, 10, 21	crio 7126	. . 3 class (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
26	2, 3, 5, 9, 25	cmpo 7172	. 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
27	1, 26	wceq 1542	1 wff |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))

This definition is referenced by:  scutval  33635  dmscut  33646  scutf  33647