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

Definition df-limits 25704
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 25680 . 2  class  Limits
2 con0 4581 . . . 4  class  On
3 cbigcup 25678 . . . . 5  class  Bigcup
43cfix 25679 . . . 4  class  Fix Bigcup
52, 4cin 3319 . . 3  class  ( On 
i^i  Fix Bigcup )
6 c0 3628 . . . 4  class  (/)
76csn 3814 . . 3  class  { (/) }
85, 7cdif 3317 . 2  class  ( ( On  i^i  Fix Bigcup ) 
\  { (/) } )
91, 8wceq 1652 1  wff  Limits  =  ( ( On  i^i  Fix Bigcup )  \  { (/) } )
Colors of variables: wff set class
This definition is referenced by:  ellimits  25755  limitssson  25756
  Copyright terms: Public domain W3C validator