Theorem hashgt0

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

	Ref	Expression
Assertion	hashgt0	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to 0<\left|A\right|$$

Proof

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