Metamath Proof Explorer

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 i^i 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 i^i Fix Bigcup )
5 c0 
 |-  (/)
6 5 csn 
 |-  { (/) }
7 4 6 cdif 
 |-  ( ( On i^i Fix Bigcup ) \ { (/) } )
8 0 7 wceq 
 |-  Limits = ( ( On i^i Fix Bigcup ) \ { (/) } )