Theorem nnfi 9009

Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5303. (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 8889	. . 3 ⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴)
2		breq2 5091	. . . 4 ⊢ (𝑥 = 𝐴 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴))
3	2	rspcev 3570	. . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ 𝐴) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4	1, 3	mpdan 684	. 2 ⊢ (𝐴 ∈ ω → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
5		isfi 8814	. 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
6	4, 5	sylibr 233	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3071   class class class wbr 5087  ωcom 7757   ≈ cen 8778  Fincfn 8781

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7628

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-om 7758  df-en 8782  df-fin 8785

This theorem is referenced by:  ssnnfi  9011  enfii  9031  phplem1  9049  phplem2  9050  php  9052  php2  9053  php3  9054  nndomog  9058  onomeneq  9070  sucdom  9077  ominf  9100  cardnn  9792  en2eqpr  9836  en2eleq  9837  infxpenlem  9842  dfac12k  9976  ficardadju  10028  pwsdompw  10033  ackbij2lem1  10048  ackbij1lem3  10051  ackbij1lem5  10053  ackbij1lem14  10062  ackbij1b  10068  fin23lem23  10155  fin23lem22  10156  domtriomlem  10271  gchdju1  10485  gch2  10504  omina  10520  hashgval2  14165  hashdom  14166  hashp1i  14190  hash1snb  14206  hash2pr  14255  pr2pwpr  14265  hash3tr  14276  xpsfrnel  17343  symggen  19147  psgnunilem1  19170  lt6abl  19564  simpgnsgd  19771  znfld  20840  frgpcyg  20853  xpsmet  23607  xpsxms  23762  xpsms  23763  isppw  26335  unidifsnel  30991  unidifsnne  30992  finxpreclem4  35621  harinf  41060  frlmpwfi  41127  infordmin  41360