Theorem hashge0

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

	Ref	Expression
Assertion	hashge0	$$⊢A\in V\to 0\le \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		0domg	$$⊢A\in V\to \varnothing \preccurlyeq A$$
2		hashdomi	$$⊢\varnothing \preccurlyeq A\to \left|\varnothing \right|\le \left|A\right|$$
3		hash0	$$⊢\left|\varnothing \right|=0$$
4	3	breq1i	$$⊢\left|\varnothing \right|\le \left|A\right|\leftrightarrow 0\le \left|A\right|$$
5	4	biimpi	$$⊢\left|\varnothing \right|\le \left|A\right|\to 0\le \left|A\right|$$
6	1 2 5	3syl	$$⊢A\in V\to 0\le \left|A\right|$$