Definition df-cuts 28176

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-cuts	⊢ |s = (𝑎 ∈ 𝒫 No, 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))

Distinct variable group:   𝑎,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-cuts

Step	Hyp	Ref	Expression
1		ccuts 28175	. 2 class |s
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		csur 28027	. . . 4 class No
5	4	cpw 4560	. . 3 class 𝒫 No
6		cslts 28173	. . . 4 class <<s
7	2	cv 1569	. . . . 5 class 𝑎
8	7	csn 4588	. . . 4 class {𝑎}
9	6, 8	cima 5658	. . 3 class ( <<s “ {𝑎})
10		vx	. . . . . . 7 setvar 𝑥
11	10	cv 1569	. . . . . 6 class 𝑥
12		cbday 28029	. . . . . 6 class bday
13	11, 12	cfv 6558	. . . . 5 class (bday‘𝑥)
14		vy	. . . . . . . . . . . 12 setvar 𝑦
15	14	cv 1569	. . . . . . . . . . 11 class 𝑦
16	15	csn 4588	. . . . . . . . . 10 class {𝑦}
17	7, 16, 6	wbr 5106	. . . . . . . . 9 wff 𝑎 <<s {𝑦}
18	3	cv 1569	. . . . . . . . . 10 class 𝑏
19	16, 18, 6	wbr 5106	. . . . . . . . 9 wff {𝑦} <<s 𝑏
20	17, 19	wa 401	. . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
21	20, 14, 4	crab 3416	. . . . . . 7 class {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
22	12, 21	cima 5658	. . . . . 6 class (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
23	22	cint 4910	. . . . 5 class ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
24	13, 23	wceq 1570	. . . 4 wff (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
25	24, 10, 21	crio 7399	. . 3 class (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
26	2, 3, 5, 9, 25	cmpo 7445	. 2 class (𝑎 ∈ 𝒫 No, 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
27	1, 26	wceq 1570	1 wff |s = (𝑎 ∈ 𝒫 No, 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))

This definition is used by:  cutsval  28196  dmcuts  28207  cutsf  28208