Theorem hashnncl

Description: Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Assertion	hashnncl	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\in \mathbb{N}\leftrightarrow A\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		nnne0	$$⊢\left|A\right|\in \mathbb{N}\to \left|A\right|\ne 0$$
2		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
3		elnn0	$$⊢\left|A\right|\in {\mathbb{N}}_0\leftrightarrow \left(\left|A\right|\in \mathbb{N}\vee \left|A\right|=0\right)$$
4	2 3	sylib	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\in \mathbb{N}\vee \left|A\right|=0\right)$$
5	4	ord	$$⊢A\in \mathrm{Fin}\to \left(\neg \left|A\right|\in \mathbb{N}\to \left|A\right|=0\right)$$
6	5	necon1ad	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\ne 0\to \left|A\right|\in \mathbb{N}\right)$$
7	1 6	impbid2	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\in \mathbb{N}\leftrightarrow \left|A\right|\ne 0\right)$$
8		hasheq0	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)$$
9	8	necon3bid	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\ne 0\leftrightarrow A\ne \varnothing \right)$$
10	7 9	bitrd	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\in \mathbb{N}\leftrightarrow A\ne \varnothing \right)$$