Theorem hashnfinnn0

Description: The size of an infinite set is not a nonnegative integer. (Contributed by Alexander van der Vekens, 21-Dec-2017) (Proof shortened by Alexander van der Vekens, 18-Jan-2018)

	Ref	Expression
Assertion	hashnfinnn0	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left|A\right|\notin {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		nnel	$$⊢\neg \left|A\right|\notin {\mathbb{N}}_0\leftrightarrow \left|A\right|\in {\mathbb{N}}_0$$
2		hashclb	$$⊢A\in V\to \left(A\in \mathrm{Fin}\leftrightarrow \left|A\right|\in {\mathbb{N}}_0\right)$$
3	2	biimprd	$$⊢A\in V\to \left(\left|A\right|\in {\mathbb{N}}_0\to A\in \mathrm{Fin}\right)$$
4	1 3	syl5bi	$$⊢A\in V\to \left(\neg \left|A\right|\notin {\mathbb{N}}_0\to A\in \mathrm{Fin}\right)$$
5	4	con1d	$$⊢A\in V\to \left(\neg A\in \mathrm{Fin}\to \left|A\right|\notin {\mathbb{N}}_0\right)$$
6	5	imp	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left|A\right|\notin {\mathbb{N}}_0$$