Theorem hashfinmndnn

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

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

Proof

Step	Hyp	Ref	Expression
1		hashfinmndnn.1	$$⊢B={\mathrm{Base}}_G$$
2		hashfinmndnn.2	$$⊢\phi \to G\in \mathrm{Mnd}$$
3		hashfinmndnn.3	$$⊢\phi \to B\in \mathrm{Fin}$$
4		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
5	3 4	syl	$$⊢\phi \to \left|B\right|\in {\mathbb{N}}_0$$
6		eqid	$$⊢0_G=0_G$$
7	1 6	mndidcl	$$⊢G\in \mathrm{Mnd}\to 0_G\in B$$
8	2 7	syl	$$⊢\phi \to 0_G\in B$$
9	8 3	hashelne0d	$$⊢\phi \to \neg \left|B\right|=0$$
10	9	neqned	$$⊢\phi \to \left|B\right|\ne 0$$
11		elnnne0	$$⊢\left|B\right|\in \mathbb{N}\leftrightarrow \left(\left|B\right|\in {\mathbb{N}}_0\wedge \left|B\right|\ne 0\right)$$
12	5 10 11	sylanbrc	$$⊢\phi \to \left|B\right|\in \mathbb{N}$$