hashneq0

Description: Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018)

		Ref	Expression
	Assertion	hashneq0	$⊢ A \in V \to (0 < \|A\| \leftrightarrow A \neq \emptyset)$

Step	Hyp	Ref	Expression
1		hashnn0pnf	$⊢ A \in V \to (\|A\| \in ℕ_{0} \lor \|A\| = +∞)$
2		nn0re	$⊢ \|A\| \in ℕ_{0} \to \|A\| \in ℝ$
3		nn0ge0	$⊢ \|A\| \in ℕ_{0} \to 0 \leq \|A\|$
4		ne0gt0	$⊢ (\|A\| \in ℝ \land 0 \leq \|A\|) \to (\|A\| \neq 0 \leftrightarrow 0 < \|A\|)$
5	2 3 4	syl2anc	$⊢ \|A\| \in ℕ_{0} \to (\|A\| \neq 0 \leftrightarrow 0 < \|A\|)$
6	5	bicomd	$⊢ \|A\| \in ℕ_{0} \to (0 < \|A\| \leftrightarrow \|A\| \neq 0)$
7		breq2	$⊢ \|A\| = +∞ \to (0 < \|A\| \leftrightarrow 0 < +∞)$
8		0ltpnf	$⊢ 0 < +∞$
9		0re	$⊢ 0 \in ℝ$
10		renepnf	$⊢ 0 \in ℝ \to 0 \neq +∞$
11	9 10	ax-mp	$⊢ 0 \neq +∞$
12	11	necomi	$⊢ +∞ \neq 0$
13	8 12	2th	$⊢ 0 < +∞ \leftrightarrow +∞ \neq 0$
14		neeq1	$⊢ \|A\| = +∞ \to (\|A\| \neq 0 \leftrightarrow +∞ \neq 0)$
15	13 14	bitr4id	$⊢ \|A\| = +∞ \to (0 < +∞ \leftrightarrow \|A\| \neq 0)$
16	7 15	bitrd	$⊢ \|A\| = +∞ \to (0 < \|A\| \leftrightarrow \|A\| \neq 0)$
17	6 16	jaoi	$⊢ (\|A\| \in ℕ_{0} \lor \|A\| = +∞) \to (0 < \|A\| \leftrightarrow \|A\| \neq 0)$
18	1 17	syl	$⊢ A \in V \to (0 < \|A\| \leftrightarrow \|A\| \neq 0)$
19		hasheq0	$⊢ A \in V \to (\|A\| = 0 \leftrightarrow A = \emptyset)$
20	19	necon3bid	$⊢ A \in V \to (\|A\| \neq 0 \leftrightarrow A \neq \emptyset)$
21	18 20	bitrd	$⊢ A \in V \to (0 < \|A\| \leftrightarrow A \neq \emptyset)$

Metamath Proof Explorer