Definition df-ons 27918

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 27917	. 2 class Ons
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1538	. . . . 5 class 𝑥
4		cright 27578	. . . . 5 class R
5	3, 4	cfv 6542	. . . 4 class ( R ‘𝑥)
6		c0 4321	. . . 4 class ∅
7	5, 6	wceq 1539	. . 3 wff ( R ‘𝑥) = ∅
8		csur 27379	. . 3 class No
9	7, 2, 8	crab 3430	. 2 class {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}
10	1, 9	wceq 1539	1 wff Ons = {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}

This definition is referenced by:  elons  27919  onssno  27920