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 5630
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 5683, dflim3 6916, 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 5626 . 2 wff Lim 𝐴
31word 5624 . . 3 wff Ord 𝐴
4 c0 3873 . . . 4 class
51, 4wne 2779 . . 3 wff 𝐴 ≠ ∅
61cuni 4366 . . . 4 class 𝐴
71, 6wceq 1474 . . 3 wff 𝐴 = 𝐴
83, 5, 7w3a 1030 . 2 wff (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴)
92, 8wb 194 1 wff (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  limeq  5637  dflim2  5683  limord  5686  limuni  5687  unizlim  5746  limon  6905  dflim3  6916  nnsuc  6951  onfununi  7302  dfrdg2  30738  ellimits  30980  onsucuni3  32174
  Copyright terms: Public domain W3C validator