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

Metamath Proof Explorer

Theorem hashclb

Description: Reverse closure of the # function. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Assertion hashclb ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) )

Proof

Step Hyp Ref Expression
1 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
2 nn0re ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ∈ ℝ )
3 pnfnre ⊢ +∞ ∉ ℝ
4 3 neli ⊢ ¬ +∞ ∈ ℝ
5 hashinf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
6 5 eleq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ∈ ℝ ↔ +∞ ∈ ℝ ) )
7 4 6 mtbiri ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ¬ ( ♯ ‘ 𝐴 ) ∈ ℝ )
8 7 ex ⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ Fin → ¬ ( ♯ ‘ 𝐴 ) ∈ ℝ ) )
9 8 con4d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∈ ℝ → 𝐴 ∈ Fin ) )
10 2 9 syl5 ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → 𝐴 ∈ Fin ) )
11 1 10 impbid2 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) )