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	|- ( ( S e. V /\ N e. NN0 ) -> ( ( # ` S ) = N -> S e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1a	|- ( N e. NN0 -> ( ( # ` S ) = N -> ( # ` S ) e. NN0 ) )
2	1	adantl	|- ( ( S e. V /\ N e. NN0 ) -> ( ( # ` S ) = N -> ( # ` S ) e. NN0 ) )
3		hashclb	|- ( S e. V -> ( S e. Fin <-> ( # ` S ) e. NN0 ) )
4	3	bicomd	|- ( S e. V -> ( ( # ` S ) e. NN0 <-> S e. Fin ) )
5	4	adantr	|- ( ( S e. V /\ N e. NN0 ) -> ( ( # ` S ) e. NN0 <-> S e. Fin ) )
6	2 5	sylibd	|- ( ( S e. V /\ N e. NN0 ) -> ( ( # ` S ) = N -> S e. Fin ) )