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}\leftrightarrow \exists n\in {\mathbb{N}}_0\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 {\mathbb{N}}_0$$
3		isfinite4	$$⊢A\in \mathrm{Fin}\leftrightarrow \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 {\mathbb{N}}_0\wedge \left(1\dots \left|A\right|\right)\approx A\right)$$
6		eleq1	$$⊢n=\left|A\right|\to \left(n\in {\mathbb{N}}_0\leftrightarrow \left|A\right|\in {\mathbb{N}}_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\leftrightarrow \left(1\dots \left|A\right|\right)\approx A\right)$$
9	6 8	anbi12d	$$⊢n=\left|A\right|\to \left(\left(n\in {\mathbb{N}}_0\wedge \left(1\dots n\right)\approx A\right)\leftrightarrow \left(\left|A\right|\in {\mathbb{N}}_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 {\mathbb{N}}_0\wedge \left(1\dots \left|A\right|\right)\approx A\right)\to \exists n\left(n\in {\mathbb{N}}_0\wedge \left(1\dots n\right)\approx A\right)\right)$$
11	1 5 10	mpsyl	$$⊢A\in \mathrm{Fin}\to \exists n\left(n\in {\mathbb{N}}_0\wedge \left(1\dots n\right)\approx A\right)$$
12		df-rex	$$⊢\exists n\in {\mathbb{N}}_0\left(1\dots n\right)\approx A\leftrightarrow \exists n\left(n\in {\mathbb{N}}_0\wedge \left(1\dots n\right)\approx A\right)$$
13	11 12	sylibr	$$⊢A\in \mathrm{Fin}\to \exists n\in {\mathbb{N}}_0\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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_0\wedge \left(1\dots n\right)\approx A\right)\to A\in \mathrm{Fin}$$
27	26	rexlimiva	$$⊢\exists n\in {\mathbb{N}}_0\left(1\dots n\right)\approx A\to A\in \mathrm{Fin}$$
28	13 27	impbii	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists n\in {\mathbb{N}}_0\left(1\dots n\right)\approx A$$