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 ⊢ B = Base G
hashfingrpnn.2 ⊢ φ → G ∈ Grp
hashfingrpnn.3 ⊢ φ → B ∈ Fin
Assertion hashfingrpnn ⊢ φ → B ∈ ℕ

Proof

Step Hyp Ref Expression
1 hashfingrpnn.1 ⊢ B = Base G
2 hashfingrpnn.2 ⊢ φ → G ∈ Grp
3 hashfingrpnn.3 ⊢ φ → B ∈ Fin
4 2 grpmndd ⊢ φ → G ∈ Mnd
5 1 4 3 hashfinmndnn ⊢ φ → B ∈ ℕ