MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vrmd Unicode version

Definition df-vrmd 14472
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.)
Assertion
Ref Expression
df-vrmd  |- varFMnd  =  ( i  e. 
_V  |->  ( j  e.  i  |->  <" j "> ) )
Distinct variable group:    i, j

Detailed syntax breakdown of Definition df-vrmd
StepHypRef Expression
1 cvrmd 14470 . 2  class varFMnd
2 vi . . 3  set  i
3 cvv 2788 . . 3  class  _V
4 vj . . . 4  set  j
52cv 1622 . . . 4  class  i
64cv 1622 . . . . 5  class  j
76cs1 11405 . . . 4  class  <" j ">
84, 5, 7cmpt 4077 . . 3  class  ( j  e.  i  |->  <" j "> )
92, 3, 8cmpt 4077 . 2  class  ( i  e.  _V  |->  ( j  e.  i  |->  <" j "> ) )
101, 9wceq 1623 1  wff varFMnd  =  ( i  e. 
_V  |->  ( j  e.  i  |->  <" j "> ) )
Colors of variables: wff set class
This definition is referenced by:  vrmdfval  14478
  Copyright terms: Public domain W3C validator