Theorem nnfi 9104

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062   class class class wbr 5100  ωcom 7818   ≈ cen 8892  Fincfn 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-om 7819  df-en 8896  df-fin 8899

This theorem is referenced by:  ssnnfi  9106  enfii  9122  phplem1  9140  phplem2  9141  php  9143  php2  9144  php3  9145  nndomog  9149  onomeneq  9150  sucdom  9156  ominf  9176  findcard3  9195  nnsdomg  9211  infsdomnn  9213  fiint  9239  cardnn  9887  en2eqpr  9929  en2eleq  9930  infxpenlem  9935  dfac12k  10070  ficardadju  10122  pwsdompw  10125  ackbij2lem1  10140  ackbij1lem3  10143  ackbij1lem5  10145  ackbij1lem14  10154  ackbij1b  10160  fin23lem23  10248  fin23lem22  10249  domtriomlem  10364  gchdju1  10579  gch2  10598  omina  10614  hashgval2  14313  hashdom  14314  hashp1i  14338  hash1snb  14354  hash2pr  14404  pr2pwpr  14414  hash3tr  14426  xpsfrnel  17495  symggen  19411  psgnunilem1  19434  lt6abl  19836  simpgnsgd  20043  znfld  21527  frgpcyg  21540  xpsmet  24338  xpsxms  24490  xpsms  24491  isppw  27092  madefi  27921  oldfi  27922  unidifsnel  32622  unidifsnne  32623  fineqvnttrclse  35302  finxpreclem4  37649  harinf  43391  frlmpwfi  43455  cantnfub2  43679  infordmin  43888