Definition df-ons 28275

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 28274	. 2 class Ons
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1539	. . . . 5 class 𝑥
4		cright 27885	. . . . 5 class R
5	3, 4	cfv 6561	. . . 4 class ( R ‘𝑥)
6		c0 4333	. . . 4 class ∅
7	5, 6	wceq 1540	. . 3 wff ( R ‘𝑥) = ∅
8		csur 27684	. . 3 class No
9	7, 2, 8	crab 3436	. 2 class {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}
10	1, 9	wceq 1540	1 wff Ons = {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅}

This definition is referenced by:  elons  28276  onssno  28277