Theorem vrmdfval

Description: The canonical injection from the generating set I to the base set of the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypothesis	vrmdfval.u	$$⊢U={var}_{\mathit{FMnd}}\left(I\right)$$
Assertion	vrmdfval	$$⊢I\in V\to U=\left(j\in I⟼⟨“j”⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		vrmdfval.u	$$⊢U={var}_{\mathit{FMnd}}\left(I\right)$$
2		df-vrmd	$$⊢{var}_{\mathit{FMnd}}=\left(i\in \mathrm{V}⟼\left(j\in i⟼⟨“j”⟩\right)\right)$$
3		mpteq1	$$⊢i=I\to \left(j\in i⟼⟨“j”⟩\right)=\left(j\in I⟼⟨“j”⟩\right)$$
4		elex	$$⊢I\in V\to I\in \mathrm{V}$$
5		mptexg	$$⊢I\in V\to \left(j\in I⟼⟨“j”⟩\right)\in \mathrm{V}$$
6	2 3 4 5	fvmptd3	$$⊢I\in V\to {var}_{\mathit{FMnd}}\left(I\right)=\left(j\in I⟼⟨“j”⟩\right)$$
7	1 6	syl5eq	$$⊢I\in V\to U=\left(j\in I⟼⟨“j”⟩\right)$$