![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnfi | Structured version Visualization version GIF version |
Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015.) Avoid ax-pow 5361. (Revised by BTernaryTau, 23-Sep-2024.) |
Ref | Expression |
---|---|
nnfi | ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enrefnn 9077 | . . 3 ⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴) | |
2 | breq2 5149 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴)) | |
3 | 2 | rspcev 3607 | . . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ 𝐴) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
4 | 1, 3 | mpdan 685 | . 2 ⊢ (𝐴 ∈ ω → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
5 | isfi 8999 | . 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) | |
6 | 4, 5 | sylibr 233 | 1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 ∃wrex 3060 class class class wbr 5145 ωcom 7868 ≈ cen 8963 Fincfn 8966 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-12 2167 ax-ext 2697 ax-sep 5296 ax-nul 5303 ax-pr 5425 ax-un 7738 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-clab 2704 df-cleq 2718 df-clel 2803 df-ne 2931 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3966 df-nul 4323 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4906 df-br 5146 df-opab 5208 df-tr 5263 df-id 5572 df-eprel 5578 df-po 5586 df-so 5587 df-fr 5629 df-we 5631 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 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 7869 df-en 8967 df-fin 8970 |
This theorem is referenced by: ssnnfi 9199 enfii 9216 phplem1 9234 phplem2 9235 php 9237 php2 9238 php3 9239 nndomog 9243 onomeneq 9255 sucdom 9262 ominf 9285 findcard3 9312 nnsdomg 9329 infsdomnn 9332 fiint 9361 cardnn 9999 en2eqpr 10043 en2eleq 10044 infxpenlem 10049 dfac12k 10183 ficardadju 10235 pwsdompw 10238 ackbij2lem1 10253 ackbij1lem3 10256 ackbij1lem5 10258 ackbij1lem14 10267 ackbij1b 10273 fin23lem23 10360 fin23lem22 10361 domtriomlem 10476 gchdju1 10690 gch2 10709 omina 10725 hashgval2 14390 hashdom 14391 hashp1i 14415 hash1snb 14431 hash2pr 14483 pr2pwpr 14493 hash3tr 14504 xpsfrnel 17572 symggen 19464 psgnunilem1 19487 lt6abl 19889 simpgnsgd 20096 znfld 21554 frgpcyg 21567 xpsmet 24376 xpsxms 24531 xpsms 24532 isppw 27139 unidifsnel 32461 unidifsnne 32462 finxpreclem4 37114 harinf 42729 frlmpwfi 42796 cantnfub2 43025 infordmin 43236 |
Copyright terms: Public domain | W3C validator |