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

Theorem limord 5927
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 5871 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1139 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wne 2943  c0 4063   cuni 4574  Ord word 5865  Lim wlim 5867
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 383  df-3an 1073  df-lim 5871
This theorem is referenced by:  0ellim  5930  limelon  5931  nlimsucg  7189  ordzsl  7192  limsuc  7196  limsssuc  7197  limomss  7217  ordom  7221  limom  7227  tfr2b  7645  rdgsucg  7672  rdglimg  7674  rdglim2  7681  oesuclem  7759  odi  7813  omeulem1  7816  oelim2  7829  oeoalem  7830  oeoelem  7832  limenpsi  8291  limensuci  8292  ordtypelem3  8581  ordtypelem5  8583  ordtypelem6  8584  ordtypelem7  8585  ordtypelem9  8587  r1tr  8803  r1ordg  8805  r1ord3g  8806  r1pwss  8811  r1val1  8813  rankwflemb  8820  r1elwf  8823  rankr1ai  8825  rankr1ag  8829  rankr1bg  8830  unwf  8837  rankr1clem  8847  rankr1c  8848  rankval3b  8853  rankonidlem  8855  onssr1  8858  coflim  9285  cflim3  9286  cflim2  9287  cfss  9289  cfslb  9290  cfslbn  9291  cfslb2n  9292  r1limwun  9760  inar1  9799  rdgprc  32036  limsucncmpi  32781
  Copyright terms: Public domain W3C validator