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

Theorem nnord 7811
Description: A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
Assertion
Ref Expression
nnord (𝐴 ∈ ω → Ord 𝐴)

Proof of Theorem nnord
StepHypRef Expression
1 nnon 7809 . 2 (𝐴 ∈ ω → 𝐴 ∈ On)
2 eloni 6328 . 2 (𝐴 ∈ On → Ord 𝐴)
31, 2syl 17 1 (𝐴 ∈ ω → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Ord word 6317  Oncon0 6318  ωcom 7803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rab 3407  df-v 3446  df-in 3918  df-ss 3928  df-uni 4867  df-tr 5224  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-ord 6321  df-on 6322  df-om 7804
This theorem is referenced by:  nnlim  7817  nnsuc  7821  omsucne  7822  nnaordi  8566  nnaord  8567  nnaword  8575  nnmord  8580  nnmwordi  8583  nnawordex  8585  omsmo  8605  eldifsucnn  8611  enrefnn  8994  dif1enlemOLD  9104  pssnn  9115  unfi  9119  phplem2  9155  php  9157  php4  9160  nndomog  9163  phplem1OLD  9164  phplem2OLD  9165  phplem3OLD  9166  phplem4OLD  9167  phpOLD  9169  nndomogOLD  9173  onomeneq  9175  ominf  9205  ominfOLD  9206  isinf  9207  isinfOLD  9208  pssnnOLD  9212  dif1ennnALT  9224  findcard3  9232  unblem1  9242  isfinite2  9248  unfilem1  9257  inf3lem5  9573  inf3lem6  9574  cantnfp1lem2  9620  cantnfp1lem3  9621  ttrcltr  9657  ttrclss  9661  dmttrcl  9662  rnttrcl  9663  ttrclselem2  9667  dif1card  9951  nnadju  10138  pwsdompw  10145  ackbij1lem5  10165  ackbij1lem14  10174  ackbij1lem16  10176  ackbij1b  10180  ackbij2  10184  sornom  10218  infpssrlem4  10247  infpssrlem5  10248  fin23lem26  10266  fin23lem23  10267  isf32lem2  10295  isf32lem3  10296  isf32lem4  10297  domtriomlem  10383  axdc3lem2  10392  axdc3lem4  10394  canthp1lem2  10594  elni2  10818  piord  10821  addnidpi  10842  indpi  10848  om2uzf1oi  13864  fzennn  13879  hashp1i  14309  bnj529  33410  bnj1098  33452  bnj570  33574  bnj594  33581  bnj580  33582  bnj967  33614  bnj1001  33628  bnj1053  33645  bnj1071  33646  nnuni  34355  hfun  34809  finminlem  34836  finxpsuclem  35914  finxpsuc  35915  wepwso  41413  dflim5  41707
  Copyright terms: Public domain W3C validator