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

Metamath Proof Explorer

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 2 grpmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
5 1 4 3 hashfinmndnn ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )