This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )