Theorem nnord 7906

Description: A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)

Assertion

Ref	Expression
nnord	⊢ (𝐴 ∈ ω → Ord 𝐴)

Proof of Theorem nnord

Step	Hyp	Ref	Expression
1		nnon 7904	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
2		eloni 6387	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	syl 18	1 ⊢ (𝐴 ∈ ω → Ord 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Ord word 6376  Oncon0 6377  ωcom 7898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rab 3417  df-v 3456  df-ss 3901  df-uni 4871  df-tr 5216  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6380  df-on 6381  df-om 7899

This theorem is used by:  nnlim  7912  nnsuc  7916  omsucne  7917  omun  7920  nnaordi  8652  nnaord  8653  nnaword  8661  nnmord  8666  nnmwordi  8669  nnawordex  8671  nnaordex2  8673  omsmo  8692  eldifsucnn  8698  enrefnn  9099  pssnn  9209  unfi  9211  phplem2  9245  php  9247  php4  9250  nndomog  9253  onomeneq  9254  ominf  9280  isinf  9281  dif1ennnALT  9293  findcard3  9299  unblem1  9309  isfinite2  9315  unfilem1  9322  inf3lem5  9657  inf3lem6  9658  cantnfp1lem2  9704  cantnfp1lem3  9705  ttrcltr  9741  ttrclss  9745  dmttrcl  9746  rnttrcl  9747  ttrclselem2  9751  hfunOLD  9943  dif1card  10113  nnadju  10300  pwsdompw  10305  ackbij1lem5  10325  ackbij1lem14  10334  ackbij1lem16  10336  ackbij1b  10340  ackbij2  10344  sornom  10379  infpssrlem4  10408  infpssrlem5  10409  fin23lem26  10427  fin23lem23  10428  isf32lem2  10456  isf32lem3  10457  isf32lem4  10458  domtriomlem  10544  axdc3lem2  10553  axdc3lem4  10555  canthp1lem2  10762  elni2  10986  piord  10989  addnidpi  11010  indpi  11016  om2uzf1oi  14120  fzennn  14135  hashp1i  14571  om2noseqf1o  28714  bnj529  35439  bnj1098  35481  bnj570  35602  bnj594  35609  bnj580  35610  bnj967  35642  bnj1001  35656  bnj1053  35673  bnj1071  35674  fineqvnttrclselem2  35889  fineqvnttrclselem3  35890  nnuni  36669  finminlem  37283  mh-inf3f1  37506  finxpsuclem  38511  finxpsuc  38512  wepwso  44241  dflim5  44521  hashnnlt  46205