MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnord Structured version   Unicode version

Theorem nnord 6482
Description: A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
Assertion
Ref Expression
nnord  |-  ( A  e.  om  ->  Ord  A )

Proof of Theorem nnord
StepHypRef Expression
1 nnon 6480 . 2  |-  ( A  e.  om  ->  A  e.  On )
2 eloni 4727 . 2  |-  ( A  e.  On  ->  Ord  A )
31, 2syl 16 1  |-  ( A  e.  om  ->  Ord  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   Ord word 4716   Oncon0 4717   omcom 6474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pr 4529  ax-un 6370
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3185  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-pss 3342  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-tp 3880  df-op 3882  df-uni 4090  df-br 4291  df-opab 4349  df-tr 4384  df-eprel 4630  df-po 4639  df-so 4640  df-fr 4677  df-we 4679  df-ord 4720  df-on 4721  df-lim 4722  df-suc 4723  df-om 6475
This theorem is referenced by:  nnlim  6487  nnsuc  6491  nnaordi  7055  nnaord  7056  nnaword  7064  nnmord  7069  nnmwordi  7072  nnawordex  7074  omsmo  7091  phplem1  7488  phplem2  7489  phplem3  7490  phplem4  7491  php  7493  php4  7496  nndomo  7502  omsucdomOLD  7504  ominf  7523  isinf  7524  pssnn  7529  dif1enOLD  7542  dif1en  7543  unblem1  7562  isfinite2  7568  unfilem1  7574  inf3lem5  7836  inf3lem6  7837  cantnfp1lem2  7885  cantnfp1lem3  7886  cantnfp1lem2OLD  7911  cantnfp1lem3OLD  7912  dif1card  8175  pwsdompw  8371  ackbij1lem5  8391  ackbij1lem14  8400  ackbij1lem16  8402  ackbij1b  8406  ackbij2  8410  sornom  8444  infpssrlem4  8473  infpssrlem5  8474  fin23lem26  8492  fin23lem23  8493  isf32lem2  8521  isf32lem3  8522  isf32lem4  8523  domtriomlem  8609  axdc3lem2  8618  axdc3lem4  8620  canthp1lem2  8818  elni2  9044  piord  9047  addnidpi  9068  indpi  9074  om2uzf1oi  11774  fzennn  11788  hashp1i  12159  hfun  28214  finminlem  28510  wepwso  29392  bnj529  31730  bnj1098  31774  bnj570  31895  bnj594  31902  bnj580  31903  bnj967  31935  bnj1001  31948  bnj1053  31964  bnj1071  31965
  Copyright terms: Public domain W3C validator