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	⊢ Ons = { 𝑥 ∈ No ∣ ( R ‘ 𝑥 ) = ∅ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cons	⊢ Ons
1		vx	⊢ 𝑥
2		csur	⊢ No
3		cright	⊢ R
4	1	cv	⊢ 𝑥
5	4 3	cfv	⊢ ( R ‘ 𝑥 )
6		c0	⊢ ∅
7	5 6	wceq	⊢ ( R ‘ 𝑥 ) = ∅
8	7 1 2	crab	⊢ { 𝑥 ∈ No ∣ ( R ‘ 𝑥 ) = ∅ }
9	0 8	wceq	⊢ Ons = { 𝑥 ∈ No ∣ ( R ‘ 𝑥 ) = ∅ }