This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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