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 e. V -> G e. Grp )

Proof

Step Hyp Ref Expression
1 frgpgrp.g 
 |-  G = ( freeGrp ` I )
2 eqid 
 |-  ( ~FG ` I ) = ( ~FG ` I )
3 1 2 frgp0 
 |-  ( I e. V -> ( G e. Grp /\ [ (/) ] ( ~FG ` I ) = ( 0g ` G ) ) )
4 3 simpld 
 |-  ( I e. V -> G e. Grp )