Theorem vrgpfval

Description: The canonical injection from the generating set I to the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	vrgpfval.r	|- .~ = ( ~FG ` I )
	vrgpfval.u	|- U = ( varFGrp ` I )
Assertion	vrgpfval	|- ( I e. V -> U = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )

Proof

Step	Hyp	Ref	Expression
1		vrgpfval.r	|- .~ = ( ~FG ` I )
2		vrgpfval.u	|- U = ( varFGrp ` I )
3		elex	|- ( I e. V -> I e. _V )
4		id	|- ( i = I -> i = I )
5		fveq2	|- ( i = I -> ( ~FG ` i ) = ( ~FG ` I ) )
6	5 1	eqtr4di	|- ( i = I -> ( ~FG ` i ) = .~ )
7	6	eceq2d	|- ( i = I -> [ <" <. j , (/) >. "> ] ( ~FG ` i ) = [ <" <. j , (/) >. "> ] .~ )
8	4 7	mpteq12dv	|- ( i = I -> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
9		df-vrgp	|- varFGrp = ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) )
10		vex	|- i e. _V
11	10	mptex	|- ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) e. _V
12	8 9 11	fvmpt3i	|- ( I e. _V -> ( varFGrp ` I ) = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
13	3 12	syl	|- ( I e. V -> ( varFGrp ` I ) = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
14	2 13	syl5eq	|- ( I e. V -> U = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )