Definition df-ons

Description: Define the surreal ordinals. These are the maximum members of each generation of surreals. Variant of definition from Conway p. 27. (Contributed by Scott Fenton, 18-Mar-2025)

	Ref	Expression
Assertion	df-ons	$$⊢{On}_s=\left\{x\in \mathrm{No}|R\left(x\right)=\varnothing \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cons	$$class{On}_s$$
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		cright	$$classR$$
4	1	cv	$$setvarx$$
5	4 3	cfv	$$classR\left(x\right)$$
6		c0	$$class\varnothing$$
7	5 6	wceq	$$wffR\left(x\right)=\varnothing$$
8	7 1 2	crab	$$class\left\{x\in \mathrm{No}|R\left(x\right)=\varnothing \right\}$$
9	0 8	wceq	$$wff{On}_s=\left\{x\in \mathrm{No}|R\left(x\right)=\varnothing \right\}$$