Definition df-frmd

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-frmd	⊢ freeMnd = ( 𝑖 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrmd	⊢ freeMnd
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		cbs	⊢ Base
4		cnx	⊢ ndx
5	4 3	cfv	⊢ ( Base ‘ ndx )
6	1	cv	⊢ 𝑖
7	6	cword	⊢ Word 𝑖
8	5 7	cop	⊢ ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩
9		cplusg	⊢ +g
10	4 9	cfv	⊢ ( +g ‘ ndx )
11		cconcat	⊢ ++
12	7 7	cxp	⊢ ( Word 𝑖 × Word 𝑖 )
13	11 12	cres	⊢ ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) )
14	10 13	cop	⊢ ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩
15	8 14	cpr	⊢ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ }
16	1 2 15	cmpt	⊢ ( 𝑖 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ } )
17	0 16	wceq	⊢ freeMnd = ( 𝑖 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , Word 𝑖 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( Word 𝑖 × Word 𝑖 ) ) ⟩ } )