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

Theorem limord 5772
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 5716 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1074 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wne 2791  c0 3907   cuni 4427  Ord word 5710  Lim wlim 5712
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 5716
This theorem is referenced by:  0ellim  5775  limelon  5776  nlimsucg  7027  ordzsl  7030  limsuc  7034  limsssuc  7035  limomss  7055  ordom  7059  limom  7065  tfr2b  7477  rdgsucg  7504  rdglimg  7506  rdglim2  7513  oesuclem  7590  odi  7644  omeulem1  7647  oelim2  7660  oeoalem  7661  oeoelem  7663  limenpsi  8120  limensuci  8121  ordtypelem3  8410  ordtypelem5  8412  ordtypelem6  8413  ordtypelem7  8414  ordtypelem9  8416  r1tr  8624  r1ordg  8626  r1ord3g  8627  r1pwss  8632  r1val1  8634  rankwflemb  8641  r1elwf  8644  rankr1ai  8646  rankr1ag  8650  rankr1bg  8651  unwf  8658  rankr1clem  8668  rankr1c  8669  rankval3b  8674  rankonidlem  8676  onssr1  8679  coflim  9068  cflim3  9069  cflim2  9070  cfss  9072  cfslb  9073  cfslbn  9074  cfslb2n  9075  r1limwun  9543  inar1  9582  rdgprc  31674  limsucncmpi  32419
  Copyright terms: Public domain W3C validator