df-scut

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)

		Ref	Expression
	Assertion	df-scut	$⊢ \|_{s} = (a \in 𝒫 No, b \in ≪_{s} [\{a\}] ⟼ (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cscut	$class \|_{s}$
1		va	$setvar a$
2		csur	$class No$
3	2	cpw	$class 𝒫 No$
4		vb	$setvar b$
5		csslt	$class ≪_{s}$
6	1	cv	$setvar a$
7	6	csn	$class \{a\}$
8	5 7	cima	$class ≪_{s} [\{a\}]$
9		vx	$setvar x$
10		vy	$setvar y$
11	10	cv	$setvar y$
12	11	csn	$class \{y\}$
13	6 12 5	wbr	$wff a ≪_{s} \{y\}$
14	4	cv	$setvar b$
15	12 14 5	wbr	$wff \{y\} ≪_{s} b$
16	13 15	wa	$wff (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)$
17	16 10 2	crab	$class \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}$
18		cbday	$class bday$
19	9	cv	$setvar x$
20	19 18	cfv	$class bday (x)$
21	18 17	cima	$class bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]$
22	21	cint	$class ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]$
23	20 22	wceq	$wff bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]$
24	23 9 17	crio	$class (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}])$
25	1 4 3 8 24	cmpo	$class (a \in 𝒫 No, b \in ≪_{s} [\{a\}] ⟼ (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))$
26	0 25	wceq	$wff \|_{s} = (a \in 𝒫 No, b \in ≪_{s} [\{a\}] ⟼ (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))$

Metamath Proof Explorer

Definition df-scut

Detailed syntax breakdown