Theorem nnfi 9205

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3067   class class class wbr 5147  ωcom 7886   ≈ cen 8980  Fincfn 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-om 7887  df-en 8984  df-fin 8987

This theorem is referenced by:  ssnnfi  9207  enfii  9223  phplem1  9241  phplem2  9242  php  9244  php2  9245  php3  9246  nndomog  9250  onomeneq  9262  sucdom  9268  ominf  9291  findcard3  9315  nnsdomg  9332  infsdomnn  9335  fiint  9363  cardnn  10000  en2eqpr  10044  en2eleq  10045  infxpenlem  10050  dfac12k  10185  ficardadju  10237  pwsdompw  10240  ackbij2lem1  10255  ackbij1lem3  10258  ackbij1lem5  10260  ackbij1lem14  10269  ackbij1b  10275  fin23lem23  10363  fin23lem22  10364  domtriomlem  10479  gchdju1  10693  gch2  10712  omina  10728  hashgval2  14413  hashdom  14414  hashp1i  14438  hash1snb  14454  hash2pr  14504  pr2pwpr  14514  hash3tr  14526  xpsfrnel  17608  symggen  19502  psgnunilem1  19525  lt6abl  19927  simpgnsgd  20134  znfld  21596  frgpcyg  21609  xpsmet  24407  xpsxms  24562  xpsms  24563  isppw  27171  madefi  27964  oldfi  27965  unidifsnel  32560  unidifsnne  32561  finxpreclem4  37376  harinf  43022  frlmpwfi  43086  cantnfub2  43311  infordmin  43521