hashclb

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

		Ref	Expression
	Assertion	hashclb	$⊢ A \in V \to (A \in Fin \leftrightarrow \|A\| \in ℕ_{0})$

Step	Hyp	Ref	Expression
1		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
2		nn0re	$⊢ \|A\| \in ℕ_{0} \to \|A\| \in ℝ$
3		pnfnre	$⊢ +∞ \notin ℝ$
4	3	neli	$⊢ \neg +∞ \in ℝ$
5		hashinf	$⊢ (A \in V \land \neg A \in Fin) \to \|A\| = +∞$
6	5	eleq1d	$⊢ (A \in V \land \neg A \in Fin) \to (\|A\| \in ℝ \leftrightarrow +∞ \in ℝ)$
7	4 6	mtbiri	$⊢ (A \in V \land \neg A \in Fin) \to \neg \|A\| \in ℝ$
8	7	ex	$⊢ A \in V \to (\neg A \in Fin \to \neg \|A\| \in ℝ)$
9	8	con4d	$⊢ A \in V \to (\|A\| \in ℝ \to A \in Fin)$
10	2 9	syl5	$⊢ A \in V \to (\|A\| \in ℕ_{0} \to A \in Fin)$
11	1 10	impbid2	$⊢ A \in V \to (A \in Fin \leftrightarrow \|A\| \in ℕ_{0})$

Metamath Proof Explorer