This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Monoids Free monoids 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 ⊢ var FMnd = i ∈ V ⟼ j ∈ i ⟼ ⟨“ j ”⟩
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cvrmd class var FMnd
1
vi setvar i
2
cvv class V
3
vj setvar j
4
1
cv setvar i
5
3
cv setvar j
6
5
cs1 class ⟨“ j ”⟩
7
3 4 6
cmpt class j ∈ i ⟼ ⟨“ j ”⟩
8
1 2 7
cmpt class i ∈ V ⟼ j ∈ i ⟼ ⟨“ j ”⟩
9
0 8
wceq wff var FMnd = i ∈ V ⟼ j ∈ i ⟼ ⟨“ j ”⟩