Theorem nnfi 9137

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054   class class class wbr 5110  ωcom 7845   ≈ cen 8918  Fincfn 8921

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-om 7846  df-en 8922  df-fin 8925

This theorem is referenced by:  ssnnfi  9139  enfii  9156  phplem1  9174  phplem2  9175  php  9177  php2  9178  php3  9179  nndomog  9183  onomeneq  9184  sucdom  9189  ominf  9212  findcard3  9236  nnsdomg  9253  infsdomnn  9256  fiint  9284  cardnn  9923  en2eqpr  9967  en2eleq  9968  infxpenlem  9973  dfac12k  10108  ficardadju  10160  pwsdompw  10163  ackbij2lem1  10178  ackbij1lem3  10181  ackbij1lem5  10183  ackbij1lem14  10192  ackbij1b  10198  fin23lem23  10286  fin23lem22  10287  domtriomlem  10402  gchdju1  10616  gch2  10635  omina  10651  hashgval2  14350  hashdom  14351  hashp1i  14375  hash1snb  14391  hash2pr  14441  pr2pwpr  14451  hash3tr  14463  xpsfrnel  17532  symggen  19407  psgnunilem1  19430  lt6abl  19832  simpgnsgd  20039  znfld  21477  frgpcyg  21490  xpsmet  24277  xpsxms  24429  xpsms  24430  isppw  27031  madefi  27831  oldfi  27832  unidifsnel  32471  unidifsnne  32472  finxpreclem4  37389  harinf  43030  frlmpwfi  43094  cantnfub2  43318  infordmin  43528