Theorem nnfi 9131

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053   class class class wbr 5107  ωcom 7842   ≈ cen 8915  Fincfn 8918

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-om 7843  df-en 8919  df-fin 8922

This theorem is referenced by:  ssnnfi  9133  enfii  9150  phplem1  9168  phplem2  9169  php  9171  php2  9172  php3  9173  nndomog  9177  onomeneq  9178  sucdom  9183  ominf  9205  findcard3  9229  nnsdomg  9246  infsdomnn  9249  fiint  9277  cardnn  9916  en2eqpr  9960  en2eleq  9961  infxpenlem  9966  dfac12k  10101  ficardadju  10153  pwsdompw  10156  ackbij2lem1  10171  ackbij1lem3  10174  ackbij1lem5  10176  ackbij1lem14  10185  ackbij1b  10191  fin23lem23  10279  fin23lem22  10280  domtriomlem  10395  gchdju1  10609  gch2  10628  omina  10644  hashgval2  14343  hashdom  14344  hashp1i  14368  hash1snb  14384  hash2pr  14434  pr2pwpr  14444  hash3tr  14456  xpsfrnel  17525  symggen  19400  psgnunilem1  19423  lt6abl  19825  simpgnsgd  20032  znfld  21470  frgpcyg  21483  xpsmet  24270  xpsxms  24422  xpsms  24423  isppw  27024  madefi  27824  oldfi  27825  unidifsnel  32464  unidifsnne  32465  finxpreclem4  37382  harinf  43023  frlmpwfi  43087  cantnfub2  43311  infordmin  43521