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 = { x e. No | ( _Right ` x ) = (/) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cons	|- On_s
1		vx	|- x
2		csur	|- No
3		cright	|- _Right
4	1	cv	|- x
5	4 3	cfv	|- ( _Right ` x )
6		c0	|- (/)
7	5 6	wceq	|- ( _Right ` x ) = (/)
8	7 1 2	crab	|- { x e. No | ( _Right ` x ) = (/) }
9	0 8	wceq	|- On_s = { x e. No | ( _Right ` x ) = (/) }