Definition df-ons 28638

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 28637	. 2 class Ons
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1569	. . . . 5 class 𝑥
4		cright 28212	. . . . 5 class R
5	3, 4	cfv 6538	. . . 4 class (R‘𝑥)
6		c0 4279	. . . 4 class ∅
7	5, 6	wceq 1570	. . 3 wff (R‘𝑥) = ∅
8		csur 27997	. . 3 class No
9	7, 2, 8	crab 3413	. 2 class {𝑥 ∈ No ∣ (R‘𝑥) = ∅}
10	1, 9	wceq 1570	1 wff Ons = {𝑥 ∈ No ∣ (R‘𝑥) = ∅}

This definition is used by:  elons  28639  onssno  28640