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

Theorem limord 6225
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 6171 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1146 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wne 2934  c0 4209   cuni 4793  Ord word 6165  Lim wlim 6167
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 210  df-an 400  df-3an 1090  df-lim 6171
This theorem is referenced by:  0ellim  6228  limelon  6229  nlimsucg  7570  ordzsl  7573  limsuc  7577  limsssuc  7578  limomss  7598  ordom  7602  limom  7608  tfr2b  8054  rdgsucg  8081  rdglimg  8083  rdglim2  8090  oesuclem  8174  odi  8229  omeulem1  8232  oelim2  8245  oeoalem  8246  oeoelem  8248  limenpsi  8735  limensuci  8736  ordtypelem3  9050  ordtypelem5  9052  ordtypelem6  9053  ordtypelem7  9054  ordtypelem9  9056  r1tr  9271  r1ordg  9273  r1ord3g  9274  r1pwss  9279  r1val1  9281  rankwflemb  9288  r1elwf  9291  rankr1ai  9293  rankr1ag  9297  rankr1bg  9298  unwf  9305  rankr1clem  9315  rankr1c  9316  rankval3b  9321  rankonidlem  9323  onssr1  9326  coflim  9754  cflim3  9755  cflim2  9756  cfss  9758  cfslb  9759  cfslbn  9760  cfslb2n  9761  r1limwun  10229  inar1  10268  rdgprc  33334  oldlim  33699  limsucncmpi  34264  grur1cld  41376
  Copyright terms: Public domain W3C validator