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	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
	vrgpfval.u	$$⊢U={var}_{\mathit{FGrp}}\left(I\right)$$
Assertion	vrgpfval	$$⊢I\in V\to U=\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)$$

Proof

Step	Hyp	Ref	Expression
1		vrgpfval.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
2		vrgpfval.u	$$⊢U={var}_{\mathit{FGrp}}\left(I\right)$$
3		elex	$$⊢I\in V\to I\in \mathrm{V}$$
4		id	$$⊢i=I\to i=I$$
5		fveq2	$$⊢i=I\to {~}_{\mathit{FG}}\left(i\right)={~}_{\mathit{FG}}\left(I\right)$$
6	5 1	eqtr4di	$$⊢i=I\to {~}_{\mathit{FG}}\left(i\right)=\underset{\dot{}}{\sim }$$
7	6	eceq2d	$$⊢i=I\to \left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)=\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }$$
8	4 7	mpteq12dv	$$⊢i=I\to \left(j\in i⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)\right)=\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)$$
9		df-vrgp	$$⊢{var}_{\mathit{FGrp}}=\left(i\in \mathrm{V}⟼\left(j\in i⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)\right)\right)$$
10		vex	$$⊢i\in \mathrm{V}$$
11	10	mptex	$$⊢\left(j\in i⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]{~}_{\mathit{FG}}\left(i\right)\right)\in \mathrm{V}$$
12	8 9 11	fvmpt3i	$$⊢I\in \mathrm{V}\to {var}_{\mathit{FGrp}}\left(I\right)=\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)$$
13	3 12	syl	$$⊢I\in V\to {var}_{\mathit{FGrp}}\left(I\right)=\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)$$
14	2 13	eqtrid	$$⊢I\in V\to U=\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)$$