Theorem frgpval

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Hypotheses	frgpval.m	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
	frgpval.b	$$⊢M=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)$$
	frgpval.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
Assertion	frgpval	$$⊢I\in V\to G=M{/}_{𝑠}\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		frgpval.m	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
2		frgpval.b	$$⊢M=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)$$
3		frgpval.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
4		elex	$$⊢I\in V\to I\in \mathrm{V}$$
5		xpeq1	$$⊢i=I\to i\times 2_{𝑜}=I\times 2_{𝑜}$$
6	5	fveq2d	$$⊢i=I\to \mathrm{freeMnd}\left(i\times 2_{𝑜}\right)=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)$$
7	6 2	eqtr4di	$$⊢i=I\to \mathrm{freeMnd}\left(i\times 2_{𝑜}\right)=M$$
8		fveq2	$$⊢i=I\to {~}_{\mathit{FG}}\left(i\right)={~}_{\mathit{FG}}\left(I\right)$$
9	8 3	eqtr4di	$$⊢i=I\to {~}_{\mathit{FG}}\left(i\right)=\underset{\dot{}}{\sim }$$
10	7 9	oveq12d	$$⊢i=I\to \mathrm{freeMnd}\left(i\times 2_{𝑜}\right){/}_{𝑠}{~}_{\mathit{FG}}\left(i\right)=M{/}_{𝑠}\underset{\dot{}}{\sim }$$
11		df-frgp	$$⊢\mathrm{freeGrp}=\left(i\in \mathrm{V}⟼\mathrm{freeMnd}\left(i\times 2_{𝑜}\right){/}_{𝑠}{~}_{\mathit{FG}}\left(i\right)\right)$$
12		ovex	$$⊢M{/}_{𝑠}\underset{\dot{}}{\sim }\in \mathrm{V}$$
13	10 11 12	fvmpt	$$⊢I\in \mathrm{V}\to \mathrm{freeGrp}\left(I\right)=M{/}_{𝑠}\underset{\dot{}}{\sim }$$
14	4 13	syl	$$⊢I\in V\to \mathrm{freeGrp}\left(I\right)=M{/}_{𝑠}\underset{\dot{}}{\sim }$$
15	1 14	syl5eq	$$⊢I\in V\to G=M{/}_{𝑠}\underset{\dot{}}{\sim }$$