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

Metamath Proof Explorer

Theorem frgpgrp

Description: The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypothesis frgpgrp.g ⊢ G = freeGrp ⁡ I
Assertion frgpgrp ⊢ I ∈ V → G ∈ Grp

Proof

Step Hyp Ref Expression
1 frgpgrp.g ⊢ G = freeGrp ⁡ I
2 eqid ⊢ ~ FG ⁡ I = ~ FG ⁡ I
3 1 2 frgp0 ⊢ I ∈ V → G ∈ Grp ∧ ∅ ~ FG ⁡ I = 0 G
4 3 simpld ⊢ I ∈ V → G ∈ Grp