Theorem frgpval

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

	Ref	Expression
Hypotheses	frgpval.m	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	frgpval.b	⊢ 𝑀 = ( freeMnd ‘ ( 𝐼 × 2o ) )
	frgpval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
Assertion	frgpval	⊢ ( 𝐼 ∈ 𝑉 → 𝐺 = ( 𝑀 /s ∼ ) )

Proof

Step	Hyp	Ref	Expression
1		frgpval.m	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2		frgpval.b	⊢ 𝑀 = ( freeMnd ‘ ( 𝐼 × 2o ) )
3		frgpval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
4		elex	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V )
5		xpeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 × 2o ) = ( 𝐼 × 2o ) )
6	5	fveq2d	⊢ ( 𝑖 = 𝐼 → ( freeMnd ‘ ( 𝑖 × 2o ) ) = ( freeMnd ‘ ( 𝐼 × 2o ) ) )
7	6 2	eqtr4di	⊢ ( 𝑖 = 𝐼 → ( freeMnd ‘ ( 𝑖 × 2o ) ) = 𝑀 )
8		fveq2	⊢ ( 𝑖 = 𝐼 → ( ~FG ‘ 𝑖 ) = ( ~FG ‘ 𝐼 ) )
9	8 3	eqtr4di	⊢ ( 𝑖 = 𝐼 → ( ~FG ‘ 𝑖 ) = ∼ )
10	7 9	oveq12d	⊢ ( 𝑖 = 𝐼 → ( ( freeMnd ‘ ( 𝑖 × 2o ) ) /s ( ~FG ‘ 𝑖 ) ) = ( 𝑀 /s ∼ ) )
11		df-frgp	⊢ freeGrp = ( 𝑖 ∈ V ↦ ( ( freeMnd ‘ ( 𝑖 × 2o ) ) /s ( ~FG ‘ 𝑖 ) ) )
12		ovex	⊢ ( 𝑀 /s ∼ ) ∈ V
13	10 11 12	fvmpt	⊢ ( 𝐼 ∈ V → ( freeGrp ‘ 𝐼 ) = ( 𝑀 /s ∼ ) )
14	4 13	syl	⊢ ( 𝐼 ∈ 𝑉 → ( freeGrp ‘ 𝐼 ) = ( 𝑀 /s ∼ ) )
15	1 14	syl5eq	⊢ ( 𝐼 ∈ 𝑉 → 𝐺 = ( 𝑀 /s ∼ ) )