Theorem hashfingrpnn

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

	Ref	Expression
Hypotheses	hashfingrpnn.1	$$⊢B={\mathrm{Base}}_G$$
	hashfingrpnn.2	$$⊢\phi \to G\in \mathrm{Grp}$$
	hashfingrpnn.3	$$⊢\phi \to B\in \mathrm{Fin}$$
Assertion	hashfingrpnn	$$⊢\phi \to \left|B\right|\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		hashfingrpnn.1	$$⊢B={\mathrm{Base}}_G$$
2		hashfingrpnn.2	$$⊢\phi \to G\in \mathrm{Grp}$$
3		hashfingrpnn.3	$$⊢\phi \to B\in \mathrm{Fin}$$
4	2	grpmndd	$$⊢\phi \to G\in \mathrm{Mnd}$$
5	1 4 3	hashfinmndnn	$$⊢\phi \to \left|B\right|\in \mathbb{N}$$