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

Definition df-vrgp 15020
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 15017 . 2  class varFGrp
2 vi . . 3  set  i
3 cvv 2788 . . 3  class  _V
4 vj . . . 4  set  j
52cv 1622 . . . 4  class  i
64cv 1622 . . . . . . 7  class  j
7 c0 3455 . . . . . . 7  class  (/)
86, 7cop 3643 . . . . . 6  class  <. j ,  (/) >.
98cs1 11405 . . . . 5  class  <" <. j ,  (/) >. ">
10 cefg 15015 . . . . . 6  class ~FG
115, 10cfv 5255 . . . . 5  class  ( ~FG  `  i
)
129, 11cec 6658 . . . 4  class  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i )
134, 5, 12cmpt 4077 . . 3  class  ( j  e.  i  |->  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i ) )
142, 3, 13cmpt 4077 . 2  class  ( i  e.  _V  |->  ( j  e.  i  |->  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
151, 14wceq 1623 1  wff varFGrp  =  ( i  e. 
_V  |->  ( j  e.  i  |->  [ <" <. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
Colors of variables: wff set class
This definition is referenced by:  vrgpfval  15075
  Copyright terms: Public domain W3C validator