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

Theorem limord 5746
Description: A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
Assertion
Ref Expression
limord (Lim 𝐴 → Ord 𝐴)

Proof of Theorem limord
StepHypRef Expression
1 df-lim 5690 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1074 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wne 2796  c0 3896   cuni 4407  Ord word 5684  Lim wlim 5686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038  df-lim 5690
This theorem is referenced by:  0ellim  5749  limelon  5750  nlimsucg  6990  ordzsl  6993  limsuc  6997  limsssuc  6998  limomss  7018  ordom  7022  limom  7028  tfr2b  7438  rdgsucg  7465  rdglimg  7467  rdglim2  7474  oesuclem  7551  odi  7605  omeulem1  7608  oelim2  7621  oeoalem  7622  oeoelem  7624  limenpsi  8080  limensuci  8081  ordtypelem3  8370  ordtypelem5  8372  ordtypelem6  8373  ordtypelem7  8374  ordtypelem9  8376  r1tr  8584  r1ordg  8586  r1ord3g  8587  r1pwss  8592  r1val1  8594  rankwflemb  8601  r1elwf  8604  rankr1ai  8606  rankr1ag  8610  rankr1bg  8611  unwf  8618  rankr1clem  8628  rankr1c  8629  rankval3b  8634  rankonidlem  8636  onssr1  8639  coflim  9028  cflim3  9029  cflim2  9030  cfss  9032  cfslb  9033  cfslbn  9034  cfslb2n  9035  r1limwun  9503  inar1  9542  rdgprc  31393  limsucncmpi  32078
  Copyright terms: Public domain W3C validator