Theorem nnfi 9194

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3089   class class class wbr 5105  ωcom 7884   ≈ cen 8981  Fincfn 8984

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-om 7885  df-en 8985  df-fin 8988

This theorem is used by:  ssnnfi  9196  enfii  9212  phplem1  9230  phplem2  9231  php  9233  php2  9234  php3  9235  nndomog  9239  onomeneq  9240  sucdom  9246  ominf  9266  findcard3  9285  nnsdomg  9302  infsdomnn  9304  fiint  9329  cardnn  10054  en2eqpr  10096  en2eleq  10097  infxpenlem  10102  dfac12k  10236  ficardadju  10288  pwsdompw  10291  ackbij2lem1  10306  ackbij1lem3  10309  ackbij1lem5  10311  ackbij1lem14  10320  ackbij1b  10326  fin23lem23  10414  fin23lem22  10415  domtriomlem  10530  gchdju1  10751  gch2  10770  omina  10786  hashgval2  14532  hashdom  14533  hashp1i  14557  hash1snb  14574  hash2pr  14624  pr2pwpr  14634  hash3tr  14646  xpsfrnel  17746  symggen  19696  psgnunilem1  19719  lt6abl  20121  simpgnsgd  20328  znfld  21878  frgpcyg  21891  xpsmet  24713  xpsxms  24865  xpsms  24866  isppw  27453  madefi  28311  oldfi  28312  unidifsnel  33185  unidifsnne  33186  fineqvnttrclse  35863  jltalephlem  35979  finxpreclem4  38457  findcard4  38772  harinf  44181  frlmpwfi  44240  cantnfub2  44464  infordmin  44673  hashnnm  46150  hashnnlt  46151