Theorem nnfi 9165

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 9056	. . 3 ⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴)
2		breq2 5107	. . . 4 ⊢ (𝑥 = 𝐴 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴))
3	2	rspcev 3576	. . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ 𝐴) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4	1, 3	mpdan 700	. 2 ⊢ (𝐴 ∈ ω → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
5		isfi 8984	. 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
6	4, 5	sylibr 237	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3086   class class class wbr 5103  ωcom 7863   ≈ cen 8952  Fincfn 8955

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 2147  ax-9 2155  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737

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 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-om 7864  df-en 8956  df-fin 8959

This theorem is used by:  ssnnfi  9167  enfii  9183  phplem1  9201  phplem2  9202  php  9204  php2  9205  php3  9206  nndomog  9210  onomeneq  9211  sucdom  9217  ominf  9237  findcard3  9256  nnsdomg  9272  infsdomnn  9274  fiint  9299  cardnn  9971  en2eqpr  10013  en2eleq  10014  infxpenlem  10019  dfac12k  10153  ficardadju  10205  pwsdompw  10208  ackbij2lem1  10223  ackbij1lem3  10226  ackbij1lem5  10228  ackbij1lem14  10237  ackbij1b  10243  fin23lem23  10331  fin23lem22  10332  domtriomlem  10447  gchdju1  10668  gch2  10687  omina  10703  hashgval2  14445  hashdom  14446  hashp1i  14470  hash1snb  14487  hash2pr  14537  pr2pwpr  14547  hash3tr  14559  xpsfrnel  17651  symggen  19600  psgnunilem1  19623  lt6abl  20025  simpgnsgd  20232  znfld  21776  frgpcyg  21789  xpsmet  24611  xpsxms  24763  xpsms  24764  isppw  27353  madefi  28181  oldfi  28182  unidifsnel  33013  unidifsnne  33014  fineqvnttrclse  35653  finxpreclem4  38151  findcard4  38466  harinf  43878  frlmpwfi  43942  cantnfub2  44166  infordmin  44375  hashnnm  45847  hashnnlt  45848