Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-limits Unicode version

Definition df-limits 24401
Description: Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
Assertion
Ref Expression
df-limits  |-  Limits  =  ( ( On  i^i  Fix Bigcup )  \  { (/) } )

Detailed syntax breakdown of Definition df-limits
StepHypRef Expression
1 climits 24379 . 2  class  Limits
2 con0 4392 . . . 4  class  On
3 cbigcup 24377 . . . . 5  class  Bigcup
43cfix 24378 . . . 4  class  Fix Bigcup
52, 4cin 3151 . . 3  class  ( On 
i^i  Fix Bigcup )
6 c0 3455 . . . 4  class  (/)
76csn 3640 . . 3  class  { (/) }
85, 7cdif 3149 . 2  class  ( ( On  i^i  Fix Bigcup ) 
\  { (/) } )
91, 8wceq 1623 1  wff  Limits  =  ( ( On  i^i  Fix Bigcup )  \  { (/) } )
Colors of variables: wff set class
This definition is referenced by:  ellimits  24450
  Copyright terms: Public domain W3C validator