Theorem vrgpval

Description: The value of the generating elements of a 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	vrgpval	$$⊢\left(I\in V\wedge A\in I\right)\to U\left(A\right)=\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }$$

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	1 2	vrgpfval	$$⊢I\in V\to U=\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)$$
4	3	fveq1d	$$⊢I\in V\to U\left(A\right)=\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)\left(A\right)$$
5		opeq1	$$⊢j=A\to ⟨j,\varnothing ⟩=⟨A,\varnothing ⟩$$
6	5	s1eqd	$$⊢j=A\to ⟨“⟨j,\varnothing ⟩”⟩=⟨“⟨A,\varnothing ⟩”⟩$$
7	6	eceq1d	$$⊢j=A\to \left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }=\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }$$
8		eqid	$$⊢\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)=\left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)$$
9	1	fvexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
10		ecexg	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}\to \left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
11	9 10	ax-mp	$$⊢\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\in \mathrm{V}$$
12	7 8 11	fvmpt	$$⊢A\in I\to \left(j\in I⟼\left[⟨“⟨j,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }\right)\left(A\right)=\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }$$
13	4 12	sylan9eq	$$⊢\left(I\in V\wedge A\in I\right)\to U\left(A\right)=\left[⟨“⟨A,\varnothing ⟩”⟩\right]\underset{\dot{}}{\sim }$$