Theorem hashne0

Description: Deduce that the size of a set is not zero. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	hashne0.1	|- ( ph -> A e. V )
	hashne0.2	|- ( ph -> A =/= (/) )
Assertion	hashne0	|- ( ph -> 0 < ( # ` A ) )

Proof

Step	Hyp	Ref	Expression
1		hashne0.1	|- ( ph -> A e. V )
2		hashne0.2	|- ( ph -> A =/= (/) )
3		hashxnn0	|- ( A e. V -> ( # ` A ) e. NN0* )
4	1 3	syl	|- ( ph -> ( # ` A ) e. NN0* )
5		hasheq0	|- ( A e. V -> ( ( # ` A ) = 0 <-> A = (/) ) )
6	5	necon3bid	|- ( A e. V -> ( ( # ` A ) =/= 0 <-> A =/= (/) ) )
7	6	biimpar	|- ( ( A e. V /\ A =/= (/) ) -> ( # ` A ) =/= 0 )
8	1 2 7	syl2anc	|- ( ph -> ( # ` A ) =/= 0 )
9		xnn0gt0	|- ( ( ( # ` A ) e. NN0* /\ ( # ` A ) =/= 0 ) -> 0 < ( # ` A ) )
10	4 8 9	syl2anc	|- ( ph -> 0 < ( # ` A ) )