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 ) )