Definition df-limits 36714

Description: Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)

Assertion

Ref	Expression
df-limits	⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅})

Detailed syntax breakdown of Definition df-limits

Step	Hyp	Ref	Expression
1		climits 36690	. 2 class Limits
2		con0 6362	. . . 4 class On
3		cbigcup 36688	. . . . 5 class Bigcup
4	3	cfix 36689	. . . 4 class Fix Bigcup
5	2, 4	cin 4089	. . 3 class (On ∩ Fix Bigcup )
6		c0 4278	. . . 4 class ∅
7	6	csn 4584	. . 3 class {∅}
8	5, 7	cdif 4045	. 2 class ((On ∩ Fix Bigcup ) ∖ {∅})
9	1, 8	wceq 1569	1 wff Limits = ((On ∩ Fix Bigcup ) ∖ {∅})

This definition is used by:  ellimits  36764  limitssson  36765