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	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) = 𝑁 → 𝑆 ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1a	⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑆 ) = 𝑁 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 ) )
2	1	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) = 𝑁 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 ) )
3		hashclb	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ∈ Fin ↔ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ) )
4	3	bicomd	⊢ ( 𝑆 ∈ 𝑉 → ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ↔ 𝑆 ∈ Fin ) )
5	4	adantr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ↔ 𝑆 ∈ Fin ) )
6	2 5	sylibd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) = 𝑁 → 𝑆 ∈ Fin ) )