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

Metamath Proof Explorer

Theorem hashgt0

Description: The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017)

Ref Expression
Assertion hashgt0 
|- ( ( A e. V /\ A =/= (/) ) -> 0 < ( # ` A ) )

Proof

Step Hyp Ref Expression
1 hashge0 
 |-  ( A e. V -> 0 <_ ( # ` A ) )
2 1 adantr 
 |-  ( ( A e. V /\ A =/= (/) ) -> 0 <_ ( # ` A ) )
3 hasheq0 
 |-  ( A e. V -> ( ( # ` A ) = 0 <-> A = (/) ) )
4 3 necon3bid 
 |-  ( A e. V -> ( ( # ` A ) =/= 0 <-> A =/= (/) ) )
5 4 biimpar 
 |-  ( ( A e. V /\ A =/= (/) ) -> ( # ` A ) =/= 0 )
6 2 5 jca 
 |-  ( ( A e. V /\ A =/= (/) ) -> ( 0 <_ ( # ` A ) /\ ( # ` A ) =/= 0 ) )
7 0xr 
 |-  0 e. RR*
8 hashxrcl 
 |-  ( A e. V -> ( # ` A ) e. RR* )
9 xrltlen 
 |-  ( ( 0 e. RR* /\ ( # ` A ) e. RR* ) -> ( 0 < ( # ` A ) <-> ( 0 <_ ( # ` A ) /\ ( # ` A ) =/= 0 ) ) )
10 7 8 9 sylancr 
 |-  ( A e. V -> ( 0 < ( # ` A ) <-> ( 0 <_ ( # ` A ) /\ ( # ` A ) =/= 0 ) ) )
11 10 biimpar 
 |-  ( ( A e. V /\ ( 0 <_ ( # ` A ) /\ ( # ` A ) =/= 0 ) ) -> 0 < ( # ` A ) )
12 6 11 syldan 
 |-  ( ( A e. V /\ A =/= (/) ) -> 0 < ( # ` A ) )