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 6368
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 6420, dflim3 7838, 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 6364 . 2 wff Lim 𝐴
31word 6362 . . 3 wff Ord 𝐴
4 c0 4321 . . . 4 class
51, 4wne 2938 . . 3 wff 𝐴 ≠ ∅
61cuni 4907 . . . 4 class 𝐴
71, 6wceq 1539 . . 3 wff 𝐴 = 𝐴
83, 5, 7w3a 1085 . 2 wff (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴)
92, 8wb 205 1 wff (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  limeq  6375  dflim2  6420  limord  6423  limuni  6424  unizlim  6486  limon  7826  dflim3  7838  nnsuc  7875  onfununi  8343  nlim1  8491  nlim2  8492  dfrdg2  35071  ellimits  35186  onsucuni3  36551  omlimcl2  42293  dflim5  42381
  Copyright terms: Public domain W3C validator