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 = ( i e. _V |-> ( j e. i |-> <" j "> ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cvrmd | |- varFMnd |
|
| 1 | vi | |- i |
|
| 2 | cvv | |- _V |
|
| 3 | vj | |- j |
|
| 4 | 1 | cv | |- i |
| 5 | 3 | cv | |- j |
| 6 | 5 | cs1 | |- <" j "> |
| 7 | 3 4 6 | cmpt | |- ( j e. i |-> <" j "> ) |
| 8 | 1 2 7 | cmpt | |- ( i e. _V |-> ( j e. i |-> <" j "> ) ) |
| 9 | 0 8 | wceq | |- varFMnd = ( i e. _V |-> ( j e. i |-> <" j "> ) ) |