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 e. W -> ( ( # ` V ) <_ 0 <-> V = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		hashge0	|- ( V e. W -> 0 <_ ( # ` V ) )
2	1	biantrud	|- ( V e. W -> ( ( # ` V ) <_ 0 <-> ( ( # ` V ) <_ 0 /\ 0 <_ ( # ` V ) ) ) )
3		hashxrcl	|- ( V e. W -> ( # ` V ) e. RR* )
4		0xr	|- 0 e. RR*
5		xrletri3	|- ( ( ( # ` V ) e. RR* /\ 0 e. RR* ) -> ( ( # ` V ) = 0 <-> ( ( # ` V ) <_ 0 /\ 0 <_ ( # ` V ) ) ) )
6	3 4 5	sylancl	|- ( V e. W -> ( ( # ` V ) = 0 <-> ( ( # ` V ) <_ 0 /\ 0 <_ ( # ` V ) ) ) )
7		hasheq0	|- ( V e. W -> ( ( # ` V ) = 0 <-> V = (/) ) )
8	2 6 7	3bitr2d	|- ( V e. W -> ( ( # ` V ) <_ 0 <-> V = (/) ) )