hashnemnf

Description: The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017)

		Ref	Expression
	Assertion	hashnemnf	$⊢ A \in V \to \|A\| \neq −∞$

Step	Hyp	Ref	Expression
1		hashnn0pnf	$⊢ A \in V \to (\|A\| \in ℕ_{0} \lor \|A\| = +∞)$
2		mnfnre	$⊢ −∞ \notin ℝ$
3		df-nel	$⊢ −∞ \notin ℝ \leftrightarrow \neg −∞ \in ℝ$
4		nn0re	$⊢ −∞ \in ℕ_{0} \to −∞ \in ℝ$
5	4	con3i	$⊢ \neg −∞ \in ℝ \to \neg −∞ \in ℕ_{0}$
6	3 5	sylbi	$⊢ −∞ \notin ℝ \to \neg −∞ \in ℕ_{0}$
7	2 6	ax-mp	$⊢ \neg −∞ \in ℕ_{0}$
8		eleq1	$⊢ \|A\| = −∞ \to (\|A\| \in ℕ_{0} \leftrightarrow −∞ \in ℕ_{0})$
9	7 8	mtbiri	$⊢ \|A\| = −∞ \to \neg \|A\| \in ℕ_{0}$
10	9	necon2ai	$⊢ \|A\| \in ℕ_{0} \to \|A\| \neq −∞$
11		pnfnemnf	$⊢ +∞ \neq −∞$
12		neeq1	$⊢ \|A\| = +∞ \to (\|A\| \neq −∞ \leftrightarrow +∞ \neq −∞)$
13	11 12	mpbiri	$⊢ \|A\| = +∞ \to \|A\| \neq −∞$
14	10 13	jaoi	$⊢ (\|A\| \in ℕ_{0} \lor \|A\| = +∞) \to \|A\| \neq −∞$
15	1 14	syl	$⊢ A \in V \to \|A\| \neq −∞$

Metamath Proof Explorer