Theorem nnfi 9136

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

Syntax hints:   → wi 4   ∈ wcel 2142  ∃wrex 3086   class class class wbr 5100  ωcom 7846   ≈ cen 8924  Fincfn 8927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-mo 2566  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-om 7847  df-en 8928  df-fin 8931

This theorem is referenced by:  ssnnfi  9138  enfii  9154  phplem1  9172  phplem2  9173  php  9175  php2  9176  php3  9177  nndomog  9181  onomeneq  9182  sucdom  9188  ominf  9208  findcard3  9227  nnsdomg  9243  infsdomnn  9245  fiint  9271  cardnn  9921  en2eqpr  9963  en2eleq  9964  infxpenlem  9969  dfac12k  10104  ficardadju  10156  pwsdompw  10159  ackbij2lem1  10174  ackbij1lem3  10177  ackbij1lem5  10179  ackbij1lem14  10188  ackbij1b  10194  fin23lem23  10283  fin23lem22  10284  domtriomlem  10399  gchdju1  10614  gch2  10633  omina  10649  hashgval2  14391  hashdom  14392  hashp1i  14416  hash1snb  14432  hash2pr  14482  pr2pwpr  14492  hash3tr  14504  xpsfrnel  17592  symggen  19510  psgnunilem1  19533  lt6abl  19935  simpgnsgd  20142  znfld  21612  frgpcyg  21625  xpsmet  24442  xpsxms  24594  xpsms  24595  isppw  27178  madefi  28006  oldfi  28007  unidifsnel  32734  unidifsnne  32735  fineqvnttrclse  35420  finxpreclem4  37888  harinf  43611  frlmpwfi  43675  cantnfub2  43899  infordmin  44108