Theorem nnfi 8441

Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.)

Assertion

Ref	Expression
nnfi	⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)

Proof of Theorem nnfi

Step	Hyp	Ref	Expression
1		onfin2 8440	. . 3 ⊢ ω = (On ∩ Fin)
2		inss2 4053	. . 3 ⊢ (On ∩ Fin) ⊆ Fin
3	1, 2	eqsstri 3853	. 2 ⊢ ω ⊆ Fin
4	3	sseli 3816	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3790  Oncon0 5976  ωcom 7343  Fincfn 8241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-om 7344  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245

This theorem is referenced by:  cardnn  9122  en2eqpr  9163  en2eleq  9164  infxpenlem  9169  dfac12k  9304  pwsdompw  9361  ackbij2lem1  9376  ackbij1lem3  9379  ackbij1lem5  9381  ackbij1lem14  9390  ackbij1b  9396  fin23lem23  9483  fin23lem22  9484  domtriomlem  9599  gchcda1  9813  gch2  9832  omina  9848  hashgval2  13482  hashdom  13483  hashp1i  13505  hash1snb  13521  hash2pr  13565  pr2pwpr  13575  hash3tr  13586  xpsfrnel  16609  symggen  18273  psgnunilem1  18296  lt6abl  18682  znfld  20304  frgpcyg  20317  xpsmet  22595  xpsxms  22747  xpsms  22748  isppw  25292  finxpreclem4  33826  harinf  38542  frlmpwfi  38609