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}_{FMnd} (I)$
	Assertion	vrmdval	$⊢ (I \in V \land A \in I) \to U (A) = ⟨“ A ”⟩$

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

Metamath Proof Explorer