Theorem nnfi 9179

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3060   class class class wbr 5119  ωcom 7859   ≈ cen 8954  Fincfn 8957

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727

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 2065  df-mo 2539  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-om 7860  df-en 8958  df-fin 8961

This theorem is referenced by:  ssnnfi  9181  enfii  9198  phplem1  9216  phplem2  9217  php  9219  php2  9220  php3  9221  nndomog  9225  onomeneq  9235  sucdom  9241  ominf  9264  findcard3  9288  nnsdomg  9305  infsdomnn  9308  fiint  9336  cardnn  9975  en2eqpr  10019  en2eleq  10020  infxpenlem  10025  dfac12k  10160  ficardadju  10212  pwsdompw  10215  ackbij2lem1  10230  ackbij1lem3  10233  ackbij1lem5  10235  ackbij1lem14  10244  ackbij1b  10250  fin23lem23  10338  fin23lem22  10339  domtriomlem  10454  gchdju1  10668  gch2  10687  omina  10703  hashgval2  14394  hashdom  14395  hashp1i  14419  hash1snb  14435  hash2pr  14485  pr2pwpr  14495  hash3tr  14507  xpsfrnel  17574  symggen  19449  psgnunilem1  19472  lt6abl  19874  simpgnsgd  20081  znfld  21519  frgpcyg  21532  xpsmet  24319  xpsxms  24471  xpsms  24472  isppw  27074  madefi  27867  oldfi  27868  unidifsnel  32462  unidifsnne  32463  finxpreclem4  37358  harinf  43005  frlmpwfi  43069  cantnfub2  43293  infordmin  43503