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

Theorem limord 5937
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 5881 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1139 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  wne 2924  c0 4050   cuni 4580  Ord word 5875  Lim wlim 5877
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 385  df-3an 1074  df-lim 5881
This theorem is referenced by:  0ellim  5940  limelon  5941  nlimsucg  7199  ordzsl  7202  limsuc  7206  limsssuc  7207  limomss  7227  ordom  7231  limom  7237  tfr2b  7653  rdgsucg  7680  rdglimg  7682  rdglim2  7689  oesuclem  7766  odi  7820  omeulem1  7823  oelim2  7836  oeoalem  7837  oeoelem  7839  limenpsi  8292  limensuci  8293  ordtypelem3  8582  ordtypelem5  8584  ordtypelem6  8585  ordtypelem7  8586  ordtypelem9  8588  r1tr  8804  r1ordg  8806  r1ord3g  8807  r1pwss  8812  r1val1  8814  rankwflemb  8821  r1elwf  8824  rankr1ai  8826  rankr1ag  8830  rankr1bg  8831  unwf  8838  rankr1clem  8848  rankr1c  8849  rankval3b  8854  rankonidlem  8856  onssr1  8859  coflim  9267  cflim3  9268  cflim2  9269  cfss  9271  cfslb  9272  cfslbn  9273  cfslb2n  9274  r1limwun  9742  inar1  9781  rdgprc  31997  limsucncmpi  32742
  Copyright terms: Public domain W3C validator