Theorem hashfingrpnn

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

	Ref	Expression
Hypotheses	hashfingrpnn.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	hashfingrpnn.2	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	hashfingrpnn.3	⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion	hashfingrpnn	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		hashfingrpnn.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		hashfingrpnn.2	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		hashfingrpnn.3	⊢ ( 𝜑 → 𝐵 ∈ Fin )
4		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
5	2 4	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6	1 5 3	hashfinmndnn	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )