Definition df-ons 28293

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.)

Assertion

Ref	Expression
df-ons	⊢ Ons = {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}

Detailed syntax breakdown of Definition df-ons

Step	Hyp	Ref	Expression
1		cons 28292	. 2 class Ons
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1536	. . . . 5 class 𝑥
4		cright 27903	. . . . 5 class R
5	3, 4	cfv 6573	. . . 4 class ( R ‘𝑥)
6		c0 4352	. . . 4 class ∅
7	5, 6	wceq 1537	. . 3 wff ( R ‘𝑥) = ∅
8		csur 27702	. . 3 class No
9	7, 2, 8	crab 3443	. 2 class {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}
10	1, 9	wceq 1537	1 wff Ons = {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}

This definition is referenced by:  elons  28294  onssno  28295