Theorem nnfi 9090

Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5308. (Revised by BTernaryTau, 23-Sep-2024.)

Assertion

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

Proof of Theorem nnfi

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		enrefnn 8981	. . 3 ⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴)
2		breq2 5100	. . . 4 ⊢ (𝑥 = 𝐴 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴))
3	2	rspcev 3574	. . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ 𝐴) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4	1, 3	mpdan 687	. 2 ⊢ (𝐴 ∈ ω → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
5		isfi 8910	. 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
6	4, 5	sylibr 234	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3058   class class class wbr 5096  ωcom 7806   ≈ cen 8878  Fincfn 8881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-om 7807  df-en 8882  df-fin 8885

This theorem is referenced by:  ssnnfi  9092  enfii  9108  phplem1  9126  phplem2  9127  php  9129  php2  9130  php3  9131  nndomog  9135  onomeneq  9136  sucdom  9142  ominf  9162  findcard3  9181  nnsdomg  9197  infsdomnn  9199  fiint  9225  cardnn  9873  en2eqpr  9915  en2eleq  9916  infxpenlem  9921  dfac12k  10056  ficardadju  10108  pwsdompw  10111  ackbij2lem1  10126  ackbij1lem3  10129  ackbij1lem5  10131  ackbij1lem14  10140  ackbij1b  10146  fin23lem23  10234  fin23lem22  10235  domtriomlem  10350  gchdju1  10565  gch2  10584  omina  10600  hashgval2  14299  hashdom  14300  hashp1i  14324  hash1snb  14340  hash2pr  14390  pr2pwpr  14400  hash3tr  14412  xpsfrnel  17481  symggen  19397  psgnunilem1  19420  lt6abl  19822  simpgnsgd  20029  znfld  21513  frgpcyg  21526  xpsmet  24324  xpsxms  24476  xpsms  24477  isppw  27078  madefi  27885  oldfi  27886  unidifsnel  32559  unidifsnne  32560  fineqvnttrclse  35229  finxpreclem4  37538  harinf  43218  frlmpwfi  43282  cantnfub2  43506  infordmin  43715