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 6366
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 6418, dflim3 7832, 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 6362 . 2 wff Lim 𝐴
31word 6360 . . 3 wff Ord 𝐴
4 c0 4321 . . . 4 class
51, 4wne 2940 . . 3 wff 𝐴 ≠ ∅
61cuni 4907 . . . 4 class 𝐴
71, 6wceq 1541 . . 3 wff 𝐴 = 𝐴
83, 5, 7w3a 1087 . 2 wff (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴)
92, 8wb 205 1 wff (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  limeq  6373  dflim2  6418  limord  6421  limuni  6422  unizlim  6484  limon  7820  dflim3  7832  nnsuc  7869  onfununi  8337  nlim1  8485  nlim2  8486  dfrdg2  34755  ellimits  34870  onsucuni3  36236  omlimcl2  41976  dflim5  42064
  Copyright terms: Public domain W3C validator