Theorem hashle00

Description: If the size of a set is less than or equal to zero, the set must be empty. (Contributed by Alexander van der Vekens, 6-Jan-2018) (Proof shortened by AV, 24-Oct-2021)

	Ref	Expression
Assertion	hashle00	$$⊢V\in W\to \left(\left|V\right|\le 0\leftrightarrow V=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		hashge0	$$⊢V\in W\to 0\le \left|V\right|$$
2	1	biantrud	$$⊢V\in W\to \left(\left|V\right|\le 0\leftrightarrow \left(\left|V\right|\le 0\wedge 0\le \left|V\right|\right)\right)$$
3		hashxrcl	$$⊢V\in W\to \left|V\right|\in {ℝ}^{*}$$
4		0xr	$$⊢0\in {ℝ}^{*}$$
5		xrletri3	$$⊢\left(\left|V\right|\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to \left(\left|V\right|=0\leftrightarrow \left(\left|V\right|\le 0\wedge 0\le \left|V\right|\right)\right)$$
6	3 4 5	sylancl	$$⊢V\in W\to \left(\left|V\right|=0\leftrightarrow \left(\left|V\right|\le 0\wedge 0\le \left|V\right|\right)\right)$$
7		hasheq0	$$⊢V\in W\to \left(\left|V\right|=0\leftrightarrow V=\varnothing \right)$$
8	2 6 7	3bitr2d	$$⊢V\in W\to \left(\left|V\right|\le 0\leftrightarrow V=\varnothing \right)$$