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

Theorem onordi 6082
 Description: An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
on.1 𝐴 ∈ On
Assertion
Ref Expression
onordi Ord 𝐴

Proof of Theorem onordi
StepHypRef Expression
1 on.1 . 2 𝐴 ∈ On
2 eloni 5988 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2ax-mp 5 1 Ord 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2107  Ord word 5977  Oncon0 5978 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400  df-in 3799  df-ss 3806  df-uni 4674  df-tr 4990  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-ord 5981  df-on 5982 This theorem is referenced by:  ontrci  6083  onirri  6084  onun2i  6093  onuniorsuci  7319  onsucssi  7321  oawordeulem  7920  omopthi  8023  bndrank  9003  rankprb  9013  rankuniss  9028  rankelun  9034  rankelpr  9035  rankelop  9036  rankmapu  9040  rankxplim3  9043  rankxpsuc  9044  cardlim  9133  carduni  9142  dfac8b  9189  alephdom2  9245  alephfp  9266  dfac12lem2  9303  pm110.643ALT  9337  cfsmolem  9429  ttukeylem6  9673  ttukeylem7  9674  unsnen  9712  efgmnvl  18515  slerec  32516  hfuni  32884  finxpsuclem  33832  pwfi2f1o  38635
 Copyright terms: Public domain W3C validator