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

Theorem limord 6325
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 6271 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1144 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wne 2943  c0 4256   cuni 4839  Ord word 6265  Lim wlim 6267
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 206  df-an 397  df-3an 1088  df-lim 6271
This theorem is referenced by:  0ellim  6328  limelon  6329  nlimsucg  7689  ordzsl  7692  limsuc  7696  limsssuc  7697  limomss  7717  trom  7721  limom  7728  tfr2b  8227  rdgsucg  8254  rdglimg  8256  rdglim2  8263  1ellim  8328  2ellim  8329  oesuclem  8355  odi  8410  omeulem1  8413  oelim2  8426  oeoalem  8427  oeoelem  8429  limenpsi  8939  limensuci  8940  ordtypelem3  9279  ordtypelem5  9281  ordtypelem6  9282  ordtypelem7  9283  ordtypelem9  9285  r1tr  9534  r1ordg  9536  r1ord3g  9537  r1pwss  9542  r1val1  9544  rankwflemb  9551  r1elwf  9554  rankr1ai  9556  rankr1ag  9560  rankr1bg  9561  unwf  9568  rankr1clem  9578  rankr1c  9579  rankval3b  9584  rankonidlem  9586  onssr1  9589  coflim  10017  cflim3  10018  cflim2  10019  cfss  10021  cfslb  10022  cfslbn  10023  cfslb2n  10024  r1limwun  10492  inar1  10531  rdgprc  33770  oldlim  34069  limsucncmpi  34634  grur1cld  41850
  Copyright terms: Public domain W3C validator