Theorem nnfi 9159

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3091   class class class wbr 5111  ωcom 7868   ≈ cen 8946  Fincfn 8949

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 2148  ax-9 2156  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742

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 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-om 7869  df-en 8950  df-fin 8953

This theorem is used by:  ssnnfi  9161  enfii  9177  phplem1  9195  phplem2  9196  php  9198  php2  9199  php3  9200  nndomog  9204  onomeneq  9205  sucdom  9211  ominf  9231  findcard3  9250  nnsdomg  9266  infsdomnn  9268  fiint  9293  cardnn  9965  en2eqpr  10007  en2eleq  10008  infxpenlem  10013  dfac12k  10147  ficardadju  10199  pwsdompw  10202  ackbij2lem1  10217  ackbij1lem3  10220  ackbij1lem5  10222  ackbij1lem14  10231  ackbij1b  10237  fin23lem23  10325  fin23lem22  10326  domtriomlem  10441  gchdju1  10658  gch2  10677  omina  10693  hashgval2  14434  hashdom  14435  hashp1i  14459  hash1snb  14476  hash2pr  14526  pr2pwpr  14536  hash3tr  14548  xpsfrnel  17640  symggen  19586  psgnunilem1  19609  lt6abl  20011  simpgnsgd  20218  znfld  21762  frgpcyg  21775  xpsmet  24592  xpsxms  24744  xpsms  24745  isppw  27331  madefi  28159  oldfi  28160  unidifsnel  32954  unidifsnne  32955  fineqvnttrclse  35596  finxpreclem4  38099  findcard4  38424  harinf  43821  frlmpwfi  43885  cantnfub2  44109  infordmin  44318  hashnnm  45790  hashnnlt  45791