This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V ∧ N ∈ ℕ 0 → S = N → S ∈ Fin

Proof

Step Hyp Ref Expression
1 eleq1a ⊢ N ∈ ℕ 0 → S = N → S ∈ ℕ 0
2 1 adantl ⊢ S ∈ V ∧ N ∈ ℕ 0 → S = N → S ∈ ℕ 0
3 hashclb ⊢ S ∈ V → S ∈ Fin ↔ S ∈ ℕ 0
4 3 bicomd ⊢ S ∈ V → S ∈ ℕ 0 ↔ S ∈ Fin
5 4 adantr ⊢ S ∈ V ∧ N ∈ ℕ 0 → S ∈ ℕ 0 ↔ S ∈ Fin
6 2 5 sylibd ⊢ S ∈ V ∧ N ∈ ℕ 0 → S = N → S ∈ Fin