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

Definition df-lim 4695
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 4746, dflim3 6428, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.)
Assertion
Ref Expression
df-lim

Detailed syntax breakdown of Definition df-lim
StepHypRef Expression
1 cA . . 3
21wlim 4691 . 2
31word 4689 . . 3
4 c0 3614 . . . 4
51, 4wne 2585 . . 3
61cuni 4066 . . . 4
71, 6wceq 1687 . . 3
83, 5, 7w3a 950 . 2
92, 8wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  limeq  4702  dflim2  4746  limord  4749  limuni  4750  unizlim  4806  limon  6417  dflim3  6428  nnsuc  6463  onfununi  6761  abianfplem  6872  dfrdg2  27311  ellimits  27643
  Copyright terms: Public domain W3C validator