| 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 5312. (Revised by BTernaryTau, 23-Sep-2024.) |
| Ref | Expression |
|---|---|
| nnfi | ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | enrefnn 9012 | . . 3 ⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴) | |
| 2 | breq2 5094 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ 𝐴)) | |
| 3 | 2 | rspcev 3572 | . . 3 ⊢ ((𝐴 ∈ ω ∧ 𝐴 ≈ 𝐴) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
| 4 | 1, 3 | mpdan 695 | . 2 ⊢ (𝐴 ∈ ω → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
| 5 | isfi 8941 | . 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) | |
| 6 | 4, 5 | sylibr 236 | 1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ Fin) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2132 ∃wrex 3076 class class class wbr 5090 ωcom 7831 ≈ cen 8909 Fincfn 8912 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-12 2202 ax-ext 2724 ax-sep 5236 ax-nul 5246 ax-pr 5380 ax-un 7703 |
| This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-sb 2081 df-mo 2556 df-clab 2731 df-cleq 2744 df-clel 2827 df-ne 2948 df-ral 3067 df-rex 3077 df-rab 3405 df-v 3446 df-dif 3898 df-un 3900 df-in 3902 df-ss 3912 df-pss 3915 df-nul 4277 df-if 4471 df-pw 4547 df-sn 4573 df-pr 4575 df-op 4579 df-uni 4856 df-br 5091 df-opab 5153 df-tr 5198 df-id 5531 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5589 df-we 5591 df-xp 5642 df-rel 5643 df-cnv 5644 df-co 5645 df-dm 5646 df-rn 5647 df-ord 6334 df-on 6335 df-lim 6336 df-suc 6337 df-fun 6508 df-fn 6509 df-f 6510 df-f1 6511 df-fo 6512 df-f1o 6513 df-om 7832 df-en 8913 df-fin 8916 |
| This theorem is referenced by: ssnnfi 9123 enfii 9139 phplem1 9157 phplem2 9158 php 9160 php2 9161 php3 9162 nndomog 9166 onomeneq 9167 sucdom 9173 ominf 9193 findcard3 9212 nnsdomg 9228 infsdomnn 9230 fiint 9256 cardnn 9907 en2eqpr 9949 en2eleq 9950 infxpenlem 9955 dfac12k 10090 ficardadju 10142 pwsdompw 10145 ackbij2lem1 10160 ackbij1lem3 10163 ackbij1lem5 10165 ackbij1lem14 10174 ackbij1b 10180 fin23lem23 10269 fin23lem22 10270 domtriomlem 10385 gchdju1 10600 gch2 10619 omina 10635 hashgval2 14377 hashdom 14378 hashp1i 14402 hash1snb 14418 hash2pr 14468 pr2pwpr 14478 hash3tr 14490 xpsfrnel 17564 symggen 19482 psgnunilem1 19505 lt6abl 19907 simpgnsgd 20114 znfld 21581 frgpcyg 21594 xpsmet 24411 xpsxms 24563 xpsms 24564 isppw 27144 madefi 27972 oldfi 27973 unidifsnel 32672 unidifsnne 32673 fineqvnttrclse 35365 finxpreclem4 37826 harinf 43549 frlmpwfi 43613 cantnfub2 43837 infordmin 44046 |
| Copyright terms: Public domain | W3C validator |