MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lim Structured version   Unicode version

Definition df-lim 4588
Description: Define the limit ordinal predicate, which is true for a non-empty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42. See dflim2 4639, dflim3 4829, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.)
Assertion
Ref Expression
df-lim  |-  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )

Detailed syntax breakdown of Definition df-lim
StepHypRef Expression
1 cA . . 3  class  A
21wlim 4584 . 2  wff  Lim  A
31word 4582 . . 3  wff  Ord  A
4 c0 3630 . . . 4  class  (/)
51, 4wne 2601 . . 3  wff  A  =/=  (/)
61cuni 4017 . . . 4  class  U. A
71, 6wceq 1653 . . 3  wff  A  = 
U. A
83, 5, 7w3a 937 . 2  wff  ( Ord 
A  /\  A  =/=  (/) 
/\  A  =  U. A )
92, 8wb 178 1  wff  ( Lim 
A  <->  ( Ord  A  /\  A  =/=  (/)  /\  A  =  U. A ) )
Colors of variables: wff set class
This definition is referenced by:  limeq  4595  dflim2  4639  limord  4642  limuni  4643  unizlim  4700  limon  4818  dflim3  4829  nnsuc  4864  onfununi  6605  abianfplem  6717  dfrdg2  25425  ellimits  25757
  Copyright terms: Public domain W3C validator