Theorem nnfi 9148

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∃wrex 3089   class class class wbr 5109  ωcom 7858   ≈ cen 8936  Fincfn 8939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-om 7859  df-en 8940  df-fin 8943

This theorem is referenced by:  ssnnfi  9150  enfii  9166  phplem1  9184  phplem2  9185  php  9187  php2  9188  php3  9189  nndomog  9193  onomeneq  9194  sucdom  9200  ominf  9220  findcard3  9239  nnsdomg  9255  infsdomnn  9257  fiint  9282  cardnn  9945  en2eqpr  9987  en2eleq  9988  infxpenlem  9993  dfac12k  10127  ficardadju  10179  pwsdompw  10182  ackbij2lem1  10197  ackbij1lem3  10200  ackbij1lem5  10202  ackbij1lem14  10211  ackbij1b  10217  fin23lem23  10305  fin23lem22  10306  domtriomlem  10421  gchdju1  10636  gch2  10655  omina  10671  hashgval2  14410  hashdom  14411  hashp1i  14435  hash1snb  14452  hash2pr  14502  pr2pwpr  14512  hash3tr  14524  xpsfrnel  17611  symggen  19535  psgnunilem1  19558  lt6abl  19960  simpgnsgd  20167  znfld  21710  frgpcyg  21723  xpsmet  24539  xpsxms  24691  xpsms  24692  isppw  27278  madefi  28106  oldfi  28107  unidifsnel  32881  unidifsnne  32882  fineqvnttrclse  35537  finxpreclem4  38060  harinf  43781  frlmpwfi  43845  cantnfub2  44069  infordmin  44278  hashnnm  45750  hashnnlt  45751