Metamath Proof Explorer


Theorem frgpgrp

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

Ref Expression
Hypothesis frgpgrp.g 𝐺 = ( freeGrp ‘ 𝐼 )
Assertion frgpgrp ( 𝐼𝑉𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 frgpgrp.g 𝐺 = ( freeGrp ‘ 𝐼 )
2 eqid ( ~FG𝐼 ) = ( ~FG𝐼 )
3 1 2 frgp0 ( 𝐼𝑉 → ( 𝐺 ∈ Grp ∧ [ ∅ ] ( ~FG𝐼 ) = ( 0g𝐺 ) ) )
4 3 simpld ( 𝐼𝑉𝐺 ∈ Grp )