hashgt0

Description: The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017)

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

Step	Hyp	Ref	Expression
1		hashge0	$⊢ A \in V \to 0 \leq \|A\|$
2	1	adantr	$⊢ (A \in V \land A \neq \emptyset) \to 0 \leq \|A\|$
3		hasheq0	$⊢ A \in V \to (\|A\| = 0 \leftrightarrow A = \emptyset)$
4	3	necon3bid	$⊢ A \in V \to (\|A\| \neq 0 \leftrightarrow A \neq \emptyset)$
5	4	biimpar	$⊢ (A \in V \land A \neq \emptyset) \to \|A\| \neq 0$
6	2 5	jca	$⊢ (A \in V \land A \neq \emptyset) \to (0 \leq \|A\| \land \|A\| \neq 0)$
7		0xr	$⊢ 0 \in ℝ^{*}$
8		hashxrcl	$⊢ A \in V \to \|A\| \in ℝ^{*}$
9		xrltlen	$⊢ (0 \in ℝ^{} \land \|A\| \in ℝ^{}) \to (0 < \|A\| \leftrightarrow (0 \leq \|A\| \land \|A\| \neq 0))$
10	7 8 9	sylancr	$⊢ A \in V \to (0 < \|A\| \leftrightarrow (0 \leq \|A\| \land \|A\| \neq 0))$
11	10	biimpar	$⊢ (A \in V \land (0 \leq \|A\| \land \|A\| \neq 0)) \to 0 < \|A\|$
12	6 11	syldan	$⊢ (A \in V \land A \neq \emptyset) \to 0 < \|A\|$

Metamath Proof Explorer