Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 0domg 
 |-  ( A e. V -> (/) ~<_ A )
2 hashdomi 
 |-  ( (/) ~<_ A -> ( # ` (/) ) <_ ( # ` A ) )
3 hash0 
 |-  ( # ` (/) ) = 0
4 3 breq1i 
 |-  ( ( # ` (/) ) <_ ( # ` A ) <-> 0 <_ ( # ` A ) )
5 4 biimpi 
 |-  ( ( # ` (/) ) <_ ( # ` A ) -> 0 <_ ( # ` A ) )
6 1 2 5 3syl 
 |-  ( A e. V -> 0 <_ ( # ` A ) )