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

Theorem limord 5701
 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 5645 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1069 1 (Lim 𝐴 → Ord 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780  ∅c0 3874  ∪ cuni 4372  Ord word 5639  Lim wlim 5641 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 196  df-an 385  df-3an 1033  df-lim 5645 This theorem is referenced by:  0ellim  5704  limelon  5705  nlimsucg  6934  ordzsl  6937  limsuc  6941  limsssuc  6942  limomss  6962  ordom  6966  limom  6972  tfr2b  7379  rdgsucg  7406  rdglimg  7408  rdglim2  7415  oesuclem  7492  odi  7546  omeulem1  7549  oelim2  7562  oeoalem  7563  oeoelem  7565  limenpsi  8020  limensuci  8021  ordtypelem3  8308  ordtypelem5  8310  ordtypelem6  8311  ordtypelem7  8312  ordtypelem9  8314  r1tr  8522  r1ordg  8524  r1ord3g  8525  r1pwss  8530  r1val1  8532  rankwflemb  8539  r1elwf  8542  rankr1ai  8544  rankr1ag  8548  rankr1bg  8549  unwf  8556  rankr1clem  8566  rankr1c  8567  rankval3b  8572  rankonidlem  8574  onssr1  8577  coflim  8966  cflim3  8967  cflim2  8968  cfss  8970  cfslb  8971  cfslbn  8972  cfslb2n  8973  r1limwun  9437  inar1  9476  rdgprc  30944  limsucncmpi  31614
 Copyright terms: Public domain W3C validator