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 6389
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 6441, dflim3 7868, 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 6385 . 2 wff Lim 𝐴
31word 6383 . . 3 wff Ord 𝐴
4 c0 4333 . . . 4 class
51, 4wne 2940 . . 3 wff 𝐴 ≠ ∅
61cuni 4907 . . . 4 class 𝐴
71, 6wceq 1540 . . 3 wff 𝐴 = 𝐴
83, 5, 7w3a 1087 . 2 wff (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴)
92, 8wb 206 1 wff (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  limeq  6396  dflim2  6441  limord  6444  limuni  6445  unizlim  6507  limon  7856  dflim3  7868  nnsuc  7905  onfununi  8381  nlim1  8527  nlim2  8528  dfrdg2  35796  ellimits  35911  onsucuni3  37368  omlimcl2  43254  dflim5  43342
  Copyright terms: Public domain W3C validator