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 ) )