Theorem vrmdval

Description: The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016)

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

Proof

Step	Hyp	Ref	Expression
1		vrmdfval.u	$$⊢U={var}_{\mathit{FMnd}}\left(I\right)$$
2	1	vrmdfval	$$⊢I\in V\to U=\left(j\in I⟼⟨“j”⟩\right)$$
3	2	adantr	$$⊢\left(I\in V\wedge A\in I\right)\to U=\left(j\in I⟼⟨“j”⟩\right)$$
4		s1eq	$$⊢j=A\to ⟨“j”⟩=⟨“A”⟩$$
5	4	adantl	$$⊢\left(\left(I\in V\wedge A\in I\right)\wedge j=A\right)\to ⟨“j”⟩=⟨“A”⟩$$
6		simpr	$$⊢\left(I\in V\wedge A\in I\right)\to A\in I$$
7		s1cl	$$⊢A\in I\to ⟨“A”⟩\in \mathrm{Word}I$$
8	7	adantl	$$⊢\left(I\in V\wedge A\in I\right)\to ⟨“A”⟩\in \mathrm{Word}I$$
9	3 5 6 8	fvmptd	$$⊢\left(I\in V\wedge A\in I\right)\to U\left(A\right)=⟨“A”⟩$$