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

Definition df-vrgp 15036
Description: Define the canonical injection from the generating set  I into the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
Assertion
Ref Expression
df-vrgp  |- varFGrp  =  ( i  e. 
_V  |->  ( j  e.  i  |->  [ <" <. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
Distinct variable group:    i, j

Detailed syntax breakdown of Definition df-vrgp
StepHypRef Expression
1 cvrgp 15033 . 2  class varFGrp
2 vi . . 3  set  i
3 cvv 2801 . . 3  class  _V
4 vj . . . 4  set  j
52cv 1631 . . . 4  class  i
64cv 1631 . . . . . . 7  class  j
7 c0 3468 . . . . . . 7  class  (/)
86, 7cop 3656 . . . . . 6  class  <. j ,  (/) >.
98cs1 11421 . . . . 5  class  <" <. j ,  (/) >. ">
10 cefg 15031 . . . . . 6  class ~FG
115, 10cfv 5271 . . . . 5  class  ( ~FG  `  i
)
129, 11cec 6674 . . . 4  class  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i )
134, 5, 12cmpt 4093 . . 3  class  ( j  e.  i  |->  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i ) )
142, 3, 13cmpt 4093 . 2  class  ( i  e.  _V  |->  ( j  e.  i  |->  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
151, 14wceq 1632 1  wff varFGrp  =  ( i  e. 
_V  |->  ( j  e.  i  |->  [ <" <. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
Colors of variables: wff set class
This definition is referenced by:  vrgpfval  15091
  Copyright terms: Public domain W3C validator