Theorem nnfi 9183

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3087   class class class wbr 5103  ωcom 7877   ≈ cen 8970  Fincfn 8973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-om 7878  df-en 8974  df-fin 8977

This theorem is used by:  ssnnfi  9185  enfii  9201  phplem1  9219  phplem2  9220  php  9222  php2  9223  php3  9224  nndomog  9228  onomeneq  9229  sucdom  9235  ominf  9255  findcard3  9274  nnsdomg  9291  infsdomnn  9293  fiint  9318  cardnn  10044  en2eqpr  10086  en2eleq  10087  infxpenlem  10092  dfac12k  10226  ficardadju  10278  pwsdompw  10281  ackbij2lem1  10296  ackbij1lem3  10299  ackbij1lem5  10301  ackbij1lem14  10310  ackbij1b  10316  fin23lem23  10404  fin23lem22  10405  domtriomlem  10520  gchdju1  10741  gch2  10760  omina  10776  hashgval2  14522  hashdom  14523  hashp1i  14547  hash1snb  14564  hash2pr  14614  pr2pwpr  14624  hash3tr  14636  xpsfrnel  17734  symggen  19684  psgnunilem1  19707  lt6abl  20109  simpgnsgd  20316  znfld  21866  frgpcyg  21879  xpsmet  24701  xpsxms  24853  xpsms  24854  isppw  27441  madefi  28299  oldfi  28300  unidifsnel  33131  unidifsnne  33132  fineqvnttrclse  35792  finxpreclem4  38317  findcard4  38632  harinf  44040  frlmpwfi  44099  cantnfub2  44323  infordmin  44532  hashnnm  46010  hashnnlt  46011