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 | ⊢ 𝑈 = ( varFMnd ‘ 𝐼 ) | |
Assertion | vrmdfval | ⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ 〈“ 𝑗 ”〉 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vrmdfval.u | ⊢ 𝑈 = ( varFMnd ‘ 𝐼 ) | |
2 | df-vrmd | ⊢ varFMnd = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ 〈“ 𝑗 ”〉 ) ) | |
3 | mpteq1 | ⊢ ( 𝑖 = 𝐼 → ( 𝑗 ∈ 𝑖 ↦ 〈“ 𝑗 ”〉 ) = ( 𝑗 ∈ 𝐼 ↦ 〈“ 𝑗 ”〉 ) ) | |
4 | elex | ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V ) | |
5 | mptexg | ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑗 ∈ 𝐼 ↦ 〈“ 𝑗 ”〉 ) ∈ V ) | |
6 | 2 3 4 5 | fvmptd3 | ⊢ ( 𝐼 ∈ 𝑉 → ( varFMnd ‘ 𝐼 ) = ( 𝑗 ∈ 𝐼 ↦ 〈“ 𝑗 ”〉 ) ) |
7 | 1 6 | syl5eq | ⊢ ( 𝐼 ∈ 𝑉 → 𝑈 = ( 𝑗 ∈ 𝐼 ↦ 〈“ 𝑗 ”〉 ) ) |