Definition df-limits

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		climits	⊢ Limits
1		con0	⊢ On
2		cbigcup	⊢ Bigcup
3	2	cfix	⊢ Fix Bigcup
4	1 3	cin	⊢ ( On ∩ Fix Bigcup )
5		c0	⊢ ∅
6	5	csn	⊢ { ∅ }
7	4 6	cdif	⊢ ( ( On ∩ Fix Bigcup ) ∖ { ∅ } )
8	0 7	wceq	⊢ Limits = ( ( On ∩ Fix Bigcup ) ∖ { ∅ } )