Theorem frgpgrp

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

	Ref	Expression
Hypothesis	frgpgrp.g	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
Assertion	frgpgrp	$$⊢I\in V\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		frgpgrp.g	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
2		eqid	$$⊢{~}_{\mathit{FG}}\left(I\right)={~}_{\mathit{FG}}\left(I\right)$$
3	1 2	frgp0	$$⊢I\in V\to \left(G\in \mathrm{Grp}\wedge \left[\varnothing \right]{~}_{\mathit{FG}}\left(I\right)=0_G\right)$$
4	3	simpld	$$⊢I\in V\to G\in \mathrm{Grp}$$