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

Metamath Proof Explorer

Theorem hashfinmndnn

Description: A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses hashfinmndnn.1 
|- B = ( Base ` G )
hashfinmndnn.2 
|- ( ph -> G e. Mnd )
hashfinmndnn.3 
|- ( ph -> B e. Fin )
Assertion hashfinmndnn 
|- ( ph -> ( # ` B ) e. NN )

Proof

Step Hyp Ref Expression
1 hashfinmndnn.1 
 |-  B = ( Base ` G )
2 hashfinmndnn.2 
 |-  ( ph -> G e. Mnd )
3 hashfinmndnn.3 
 |-  ( ph -> B e. Fin )
4 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
5 3 4 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 1 6 mndidcl 
 |-  ( G e. Mnd -> ( 0g ` G ) e. B )
8 2 7 syl 
 |-  ( ph -> ( 0g ` G ) e. B )
9 8 3 hashelne0d 
 |-  ( ph -> -. ( # ` B ) = 0 )
10 9 neqned 
 |-  ( ph -> ( # ` B ) =/= 0 )
11 elnnne0 
 |-  ( ( # ` B ) e. NN <-> ( ( # ` B ) e. NN0 /\ ( # ` B ) =/= 0 ) )
12 5 10 11 sylanbrc 
 |-  ( ph -> ( # ` B ) e. NN )