Theorem nnfi 7052

Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.)

Assertion

Ref	Expression
nnfi	⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)

Proof of Theorem nnfi

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		enrefg 6930	. . 3 ⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴)
2		breq2 4088	. . . 4 ⊢ (𝑥 = 𝐴 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴))
3	2	rspcev 2908	. . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ 𝐴) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4	1, 3	mpdan 421	. 2 ⊢ (𝐴 ∈ ω → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
5		isfi 6927	. 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
6	4, 5	sylibr 134	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2200  ∃wrex 2509   class class class wbr 4084  ωcom 4684   ≈ cen 6900  Fincfn 6902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4203  ax-pow 4260  ax-pr 4295  ax-un 4526

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-br 4085  df-opab 4147  df-id 4386  df-xp 4727  df-rel 4728  df-cnv 4729  df-co 4730  df-dm 4731  df-rn 4732  df-res 4733  df-ima 4734  df-fun 5324  df-fn 5325  df-f 5326  df-f1 5327  df-fo 5328  df-f1o 5329  df-en 6903  df-fin 6905

This theorem is referenced by:  dif1en  7059  0fi  7064  findcard2  7069  findcard2s  7070  diffisn  7073  pw1fin  7093  en1eqsn  7136  nninfwlpoimlemg  7363  nninfwlpoimlemginf  7364  exmidonfinlem  7392  fzfig  10680  hashennnuni  11029  hashennn  11030  hashun  11055  hashp1i  11061  hash2en  11094  unct  13050  xpsfrnel  13414  znidom  14658  znidomb  14659  upgrfi  15939  pw1ninf  16500  pwf1oexmid  16510