Metamath Proof Explorer


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 = (/) ) )