Theorem hashclb

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

	Ref	Expression
Assertion	hashclb	$$⊢A\in V\to \left(A\in \mathrm{Fin}\leftrightarrow \left|A\right|\in {\mathbb{N}}_0\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
2		nn0re	$$⊢\left|A\right|\in {\mathbb{N}}_0\to \left|A\right|\in ℝ$$
3		pnfnre	$$⊢\mathrm{+\infty }\notin ℝ$$
4	3	neli	$$⊢\neg \mathrm{+\infty }\in ℝ$$
5		hashinf	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left|A\right|=\mathrm{+\infty }$$
6	5	eleq1d	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left(\left|A\right|\in ℝ\leftrightarrow \mathrm{+\infty }\in ℝ\right)$$
7	4 6	mtbiri	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \neg \left|A\right|\in ℝ$$
8	7	ex	$$⊢A\in V\to \left(\neg A\in \mathrm{Fin}\to \neg \left|A\right|\in ℝ\right)$$
9	8	con4d	$$⊢A\in V\to \left(\left|A\right|\in ℝ\to A\in \mathrm{Fin}\right)$$
10	2 9	syl5	$$⊢A\in V\to \left(\left|A\right|\in {\mathbb{N}}_0\to A\in \mathrm{Fin}\right)$$
11	1 10	impbid2	$$⊢A\in V\to \left(A\in \mathrm{Fin}\leftrightarrow \left|A\right|\in {\mathbb{N}}_0\right)$$