Metamath Proof Explorer

Theorem rp-isfinite5

Description: A set is said to be finite if it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN0 . (Contributed by RP, 3-Mar-2020)

Ref Expression
Assertion rp-isfinite5 ${⊢}{A}\in \mathrm{Fin}↔\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(1\dots {n}\right)\approx {A}$

Proof

Step Hyp Ref Expression
1 fvex ${⊢}\left|{A}\right|\in \mathrm{V}$
2 hashcl ${⊢}{A}\in \mathrm{Fin}\to \left|{A}\right|\in {ℕ}_{0}$
3 isfinite4 ${⊢}{A}\in \mathrm{Fin}↔\left(1\dots \left|{A}\right|\right)\approx {A}$
4 3 biimpi ${⊢}{A}\in \mathrm{Fin}\to \left(1\dots \left|{A}\right|\right)\approx {A}$
5 2 4 jca ${⊢}{A}\in \mathrm{Fin}\to \left(\left|{A}\right|\in {ℕ}_{0}\wedge \left(1\dots \left|{A}\right|\right)\approx {A}\right)$
6 eleq1 ${⊢}{n}=\left|{A}\right|\to \left({n}\in {ℕ}_{0}↔\left|{A}\right|\in {ℕ}_{0}\right)$
7 oveq2 ${⊢}{n}=\left|{A}\right|\to \left(1\dots {n}\right)=\left(1\dots \left|{A}\right|\right)$
8 7 breq1d ${⊢}{n}=\left|{A}\right|\to \left(\left(1\dots {n}\right)\approx {A}↔\left(1\dots \left|{A}\right|\right)\approx {A}\right)$
9 6 8 anbi12d ${⊢}{n}=\left|{A}\right|\to \left(\left({n}\in {ℕ}_{0}\wedge \left(1\dots {n}\right)\approx {A}\right)↔\left(\left|{A}\right|\in {ℕ}_{0}\wedge \left(1\dots \left|{A}\right|\right)\approx {A}\right)\right)$
10 9 spcegv ${⊢}\left|{A}\right|\in \mathrm{V}\to \left(\left(\left|{A}\right|\in {ℕ}_{0}\wedge \left(1\dots \left|{A}\right|\right)\approx {A}\right)\to \exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}\wedge \left(1\dots {n}\right)\approx {A}\right)\right)$
11 1 5 10 mpsyl ${⊢}{A}\in \mathrm{Fin}\to \exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}\wedge \left(1\dots {n}\right)\approx {A}\right)$
12 df-rex ${⊢}\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(1\dots {n}\right)\approx {A}↔\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}\wedge \left(1\dots {n}\right)\approx {A}\right)$
13 11 12 sylibr ${⊢}{A}\in \mathrm{Fin}\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(1\dots {n}\right)\approx {A}$
14 hasheni ${⊢}\left(1\dots {n}\right)\approx {A}\to \left|\left(1\dots {n}\right)\right|=\left|{A}\right|$
15 14 eqcomd ${⊢}\left(1\dots {n}\right)\approx {A}\to \left|{A}\right|=\left|\left(1\dots {n}\right)\right|$
16 hashfz1 ${⊢}{n}\in {ℕ}_{0}\to \left|\left(1\dots {n}\right)\right|={n}$
17 ovex ${⊢}\left(1\dots \left|{A}\right|\right)\in \mathrm{V}$
18 eqtr ${⊢}\left(\left|{A}\right|=\left|\left(1\dots {n}\right)\right|\wedge \left|\left(1\dots {n}\right)\right|={n}\right)\to \left|{A}\right|={n}$
19 oveq2 ${⊢}\left|{A}\right|={n}\to \left(1\dots \left|{A}\right|\right)=\left(1\dots {n}\right)$
20 eqeng ${⊢}\left(1\dots \left|{A}\right|\right)\in \mathrm{V}\to \left(\left(1\dots \left|{A}\right|\right)=\left(1\dots {n}\right)\to \left(1\dots \left|{A}\right|\right)\approx \left(1\dots {n}\right)\right)$
21 19 20 syl5 ${⊢}\left(1\dots \left|{A}\right|\right)\in \mathrm{V}\to \left(\left|{A}\right|={n}\to \left(1\dots \left|{A}\right|\right)\approx \left(1\dots {n}\right)\right)$
22 17 18 21 mpsyl ${⊢}\left(\left|{A}\right|=\left|\left(1\dots {n}\right)\right|\wedge \left|\left(1\dots {n}\right)\right|={n}\right)\to \left(1\dots \left|{A}\right|\right)\approx \left(1\dots {n}\right)$
23 15 16 22 syl2anr ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(1\dots {n}\right)\approx {A}\right)\to \left(1\dots \left|{A}\right|\right)\approx \left(1\dots {n}\right)$
24 entr ${⊢}\left(\left(1\dots \left|{A}\right|\right)\approx \left(1\dots {n}\right)\wedge \left(1\dots {n}\right)\approx {A}\right)\to \left(1\dots \left|{A}\right|\right)\approx {A}$
25 23 24 sylancom ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(1\dots {n}\right)\approx {A}\right)\to \left(1\dots \left|{A}\right|\right)\approx {A}$
26 25 3 sylibr ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(1\dots {n}\right)\approx {A}\right)\to {A}\in \mathrm{Fin}$
27 26 rexlimiva ${⊢}\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(1\dots {n}\right)\approx {A}\to {A}\in \mathrm{Fin}$
28 13 27 impbii ${⊢}{A}\in \mathrm{Fin}↔\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(1\dots {n}\right)\approx {A}$