Theorem hashfinmndnn

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

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

Proof

Step	Hyp	Ref	Expression
1		hashfinmndnn.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		hashfinmndnn.2	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
3		hashfinmndnn.3	⊢ ( 𝜑 → 𝐵 ∈ Fin )
4		hashcl	⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
5	3 4	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
6		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7	1 6	mndidcl	⊢ ( 𝐺 ∈ Mnd → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
8	2 7	syl	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
9	8 3	hashelne0d	⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝐵 ) = 0 )
10	9	neqned	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ≠ 0 )
11		elnnne0	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ≠ 0 ) )
12	5 10 11	sylanbrc	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )