Theorem nnord 7873

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 7871	. 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
2		eloni 6371	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	syl 18	1 ⊢ (𝐴 ∈ ω → Ord 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ord word 6360  Oncon0 6361  ωcom 7865

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rab 3415  df-v 3455  df-ss 3919  df-uni 4871  df-tr 5217  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365  df-om 7866

This theorem is used by:  nnlim  7879  nnsuc  7883  omsucne  7884  omun  7887  nnaordi  8609  nnaord  8610  nnaword  8618  nnmord  8623  nnmwordi  8626  nnawordex  8628  nnaordex2  8630  omsmo  8649  eldifsucnn  8655  enrefnn  9056  pssnn  9166  unfi  9168  phplem2  9202  php  9204  php4  9207  nndomog  9210  onomeneq  9211  ominf  9237  isinf  9238  dif1ennnALT  9250  findcard3  9256  unblem1  9265  isfinite2  9271  unfilem1  9278  inf3lem5  9614  inf3lem6  9615  cantnfp1lem2  9661  cantnfp1lem3  9662  ttrcltr  9698  ttrclss  9702  dmttrcl  9703  rnttrcl  9704  ttrclselem2  9708  dif1card  10016  nnadju  10203  pwsdompw  10208  ackbij1lem5  10228  ackbij1lem14  10237  ackbij1lem16  10239  ackbij1b  10243  ackbij2  10247  sornom  10282  infpssrlem4  10311  infpssrlem5  10312  fin23lem26  10330  fin23lem23  10331  isf32lem2  10359  isf32lem3  10360  isf32lem4  10361  domtriomlem  10447  axdc3lem2  10456  axdc3lem4  10458  canthp1lem2  10665  elni2  10889  piord  10892  addnidpi  10913  indpi  10919  om2uzf1oi  14019  fzennn  14034  hashp1i  14469  om2noseqf1o  28564  bnj529  35238  bnj1098  35280  bnj570  35401  bnj594  35408  bnj580  35409  bnj967  35441  bnj1001  35455  bnj1053  35472  bnj1071  35473  fineqvnttrclselem2  35635  fineqvnttrclselem3  35636  nnuni  36293  hfun  36745  finminlem  36924  mh-inf3f1  37147  finxpsuclem  38138  finxpsuc  38139  wepwso  43871  dflim5  44157  hashnnlt  45832