Theorem hashvnfin

Description: A set of finite size is a finite set. (Contributed by Alexander van der Vekens, 8-Dec-2017)

	Ref	Expression
Assertion	hashvnfin	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(\left|S\right|=N\to S\in \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1a	$$⊢N\in {\mathbb{N}}_0\to \left(\left|S\right|=N\to \left|S\right|\in {\mathbb{N}}_0\right)$$
2	1	adantl	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(\left|S\right|=N\to \left|S\right|\in {\mathbb{N}}_0\right)$$
3		hashclb	$$⊢S\in V\to \left(S\in \mathrm{Fin}\leftrightarrow \left|S\right|\in {\mathbb{N}}_0\right)$$
4	3	bicomd	$$⊢S\in V\to \left(\left|S\right|\in {\mathbb{N}}_0\leftrightarrow S\in \mathrm{Fin}\right)$$
5	4	adantr	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(\left|S\right|\in {\mathbb{N}}_0\leftrightarrow S\in \mathrm{Fin}\right)$$
6	2 5	sylibd	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to \left(\left|S\right|=N\to S\in \mathrm{Fin}\right)$$