Theorem hashfingrpnn

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

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

Proof

Step	Hyp	Ref	Expression
1		hashfingrpnn.1	|- B = ( Base ` G )
2		hashfingrpnn.2	|- ( ph -> G e. Grp )
3		hashfingrpnn.3	|- ( ph -> B e. Fin )
4		grpmnd	|- ( G e. Grp -> G e. Mnd )
5	2 4	syl	|- ( ph -> G e. Mnd )
6	1 5 3	hashfinmndnn	|- ( ph -> ( # ` B ) e. NN )