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

Metamath Proof Explorer

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