Theorem elnn 7621

Description: A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.)

Assertion

Ref	Expression
elnn	⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)

Proof of Theorem elnn

Step	Hyp	Ref	Expression
1		ordom 7620	. 2 ⊢ Ord ω
2		ordtr 6196	. 2 ⊢ (Ord ω → Tr ω)
3		trel 5153	. 2 ⊢ (Tr ω → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω))
4	1, 2, 3	mp2b 10	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2114  Tr wtr 5146  Ord word 6181  ωcom 7611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-11 2162  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306  ax-un 7491

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ne 2936  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3402  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-tr 5147  df-eprel 5444  df-po 5452  df-so 5453  df-fr 5493  df-we 5495  df-ord 6185  df-on 6186  df-lim 6187  df-om 7612

This theorem is referenced by:  nnaordi  8287  nnmordi  8300  pssnn  8779  ssnnfi  8780  ssnnfiOLD  8781  pssnnOLD  8827  unfilem1  8868  unfilem2  8869  inf3lem5  9180  cantnflt  9220  cantnfp1lem3  9228  cantnflem1d  9236  cantnflem1  9237  cnfcomlem  9247  cnfcom  9248  infpssrlem4  9818  axdc3lem2  9963  pwfseqlem3  10172  bnj1098  32346  bnj517  32448  bnj594  32475  bnj1001  32522  bnj1118  32547  bnj1128  32553  bnj1145  32556  elhf2  34132  hfelhf  34138