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

Theorem limord 6244
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 6190 . 2 (Lim 𝐴 ↔ (Ord 𝐴𝐴 ≠ ∅ ∧ 𝐴 = 𝐴))
21simp1bi 1137 1 (Lim 𝐴 → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3016  c0 4290   cuni 4832  Ord word 6184  Lim wlim 6186
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 208  df-an 397  df-3an 1081  df-lim 6190
This theorem is referenced by:  0ellim  6247  limelon  6248  nlimsucg  7545  ordzsl  7548  limsuc  7552  limsssuc  7553  limomss  7573  ordom  7577  limom  7583  tfr2b  8023  rdgsucg  8050  rdglimg  8052  rdglim2  8059  oesuclem  8141  odi  8195  omeulem1  8198  oelim2  8211  oeoalem  8212  oeoelem  8214  limenpsi  8681  limensuci  8682  ordtypelem3  8973  ordtypelem5  8975  ordtypelem6  8976  ordtypelem7  8977  ordtypelem9  8979  r1tr  9194  r1ordg  9196  r1ord3g  9197  r1pwss  9202  r1val1  9204  rankwflemb  9211  r1elwf  9214  rankr1ai  9216  rankr1ag  9220  rankr1bg  9221  unwf  9228  rankr1clem  9238  rankr1c  9239  rankval3b  9244  rankonidlem  9246  onssr1  9249  coflim  9672  cflim3  9673  cflim2  9674  cfss  9676  cfslb  9677  cfslbn  9678  cfslb2n  9679  r1limwun  10147  inar1  10186  rdgprc  32937  limsucncmpi  33691  grur1cld  40448
  Copyright terms: Public domain W3C validator