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 )