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		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
2		isfinite4	$$⊢A\in \mathrm{Fin}\leftrightarrow \left(1\dots \left|A\right|\right)\approx A$$
3	2	biimpi	$$⊢A\in \mathrm{Fin}\to \left(1\dots \left|A\right|\right)\approx A$$
4	1 3	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)$$
5		eleq1	$$⊢n=\left|A\right|\to \left(n\in {\mathbb{N}}_0\leftrightarrow \left|A\right|\in {\mathbb{N}}_0\right)$$
6		oveq2	$$⊢n=\left|A\right|\to \left(1\dots n\right)=\left(1\dots \left|A\right|\right)$$
7	6	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)$$
8	5 7	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)$$
9	1 4 8	spcedv	$$⊢A\in \mathrm{Fin}\to \exists n\left(n\in {\mathbb{N}}_0\wedge \left(1\dots n\right)\approx A\right)$$
10		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)$$
11	9 10	sylibr	$$⊢A\in \mathrm{Fin}\to \exists n\in {\mathbb{N}}_0\left(1\dots n\right)\approx A$$
12		hasheni	$$⊢\left(1\dots n\right)\approx A\to \left|\left(1\dots n\right)\right|=\left|A\right|$$
13	12	eqcomd	$$⊢\left(1\dots n\right)\approx A\to \left|A\right|=\left|\left(1\dots n\right)\right|$$
14		hashfz1	$$⊢n\in {\mathbb{N}}_0\to \left|\left(1\dots n\right)\right|=n$$
15		ovex	$$⊢\left(1\dots \left|A\right|\right)\in \mathrm{V}$$
16		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$$
17		oveq2	$$⊢\left|A\right|=n\to \left(1\dots \left|A\right|\right)=\left(1\dots n\right)$$
18		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)$$
19	17 18	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)$$
20	15 16 19	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)$$
21	13 14 20	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)$$
22		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$$
23	21 22	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$$
24	23 2	sylibr	$$⊢\left(n\in {\mathbb{N}}_0\wedge \left(1\dots n\right)\approx A\right)\to A\in \mathrm{Fin}$$
25	24	rexlimiva	$$⊢\exists n\in {\mathbb{N}}_0\left(1\dots n\right)\approx A\to A\in \mathrm{Fin}$$
26	11 25	impbii	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists n\in {\mathbb{N}}_0\left(1\dots n\right)\approx A$$