This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-vrmd

Description: Define a free monoid over a set i of generators, defined as the set of finite strings on I with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion df-vrmd varFMnd = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ⟨“ 𝑗 ”⟩ ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvrmd ⊢ varFMnd
1 vi ⊢ 𝑖
2 cvv ⊢ V
3 vj ⊢ 𝑗
4 1 cv ⊢ 𝑖
5 3 cv ⊢ 𝑗
6 5 cs1 ⊢ ⟨“ 𝑗 ”⟩
7 3 4 6 cmpt ⊢ ( 𝑗 ∈ 𝑖 ↦ ⟨“ 𝑗 ”⟩ )
8 1 2 7 cmpt ⊢ ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ⟨“ 𝑗 ”⟩ ) )
9 0 8 wceq ⊢ varFMnd = ( 𝑖 ∈ V ↦ ( 𝑗 ∈ 𝑖 ↦ ⟨“ 𝑗 ”⟩ ) )