Theorem nnfi 9081

Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5304. (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 8972	. . 3 ⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴)
2		breq2 5096	. . . 4 ⊢ (𝑥 = 𝐴 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴))
3	2	rspcev 3577	. . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ 𝐴) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4	1, 3	mpdan 687	. 2 ⊢ (𝐴 ∈ ω → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
5		isfi 8901	. 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
6	4, 5	sylibr 234	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053   class class class wbr 5092  ωcom 7799   ≈ cen 8869  Fincfn 8872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-om 7800  df-en 8873  df-fin 8876

This theorem is referenced by:  ssnnfi  9083  enfii  9100  phplem1  9118  phplem2  9119  php  9121  php2  9122  php3  9123  nndomog  9127  onomeneq  9128  sucdom  9133  ominf  9153  findcard3  9172  nnsdomg  9188  infsdomnn  9190  fiint  9216  cardnn  9859  en2eqpr  9901  en2eleq  9902  infxpenlem  9907  dfac12k  10042  ficardadju  10094  pwsdompw  10097  ackbij2lem1  10112  ackbij1lem3  10115  ackbij1lem5  10117  ackbij1lem14  10126  ackbij1b  10132  fin23lem23  10220  fin23lem22  10221  domtriomlem  10336  gchdju1  10550  gch2  10569  omina  10585  hashgval2  14285  hashdom  14286  hashp1i  14310  hash1snb  14326  hash2pr  14376  pr2pwpr  14386  hash3tr  14398  xpsfrnel  17466  symggen  19349  psgnunilem1  19372  lt6abl  19774  simpgnsgd  19981  znfld  21467  frgpcyg  21480  xpsmet  24268  xpsxms  24420  xpsms  24421  isppw  27022  madefi  27827  oldfi  27828  unidifsnel  32479  unidifsnne  32480  fineqvnttrclse  35077  finxpreclem4  37372  harinf  43011  frlmpwfi  43075  cantnfub2  43299  infordmin  43509