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

Definition df-lim 6390
Description: Define the limit ordinal predicate, which is true for a nonempty 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 6442, dflim3 7867, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.)
Assertion
Ref Expression
df-lim (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))

Detailed syntax breakdown of Definition df-lim
StepHypRef Expression
1 cA . . 3 class 𝐴
21wlim 6386 . 2 wff Lim 𝐴
31word 6384 . . 3 wff Ord 𝐴
4 c0 4338 . . . 4 class
51, 4wne 2937 . . 3 wff 𝐴 ≠ ∅
61cuni 4911 . . . 4 class 𝐴
71, 6wceq 1536 . . 3 wff 𝐴 = 𝐴
83, 5, 7w3a 1086 . 2 wff (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴)
92, 8wb 206 1 wff (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  limeq  6397  dflim2  6442  limord  6445  limuni  6446  unizlim  6508  limon  7855  dflim3  7867  nnsuc  7904  onfununi  8379  nlim1  8525  nlim2  8526  dfrdg2  35776  ellimits  35891  onsucuni3  37349  omlimcl2  43230  dflim5  43318
  Copyright terms: Public domain W3C validator