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

Definition df-vrgp 15335
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 15332 . 2  class varFGrp
2 vi . . 3  set  i
3 cvv 2948 . . 3  class  _V
4 vj . . . 4  set  j
52cv 1651 . . . 4  class  i
64cv 1651 . . . . . . 7  class  j
7 c0 3620 . . . . . . 7  class  (/)
86, 7cop 3809 . . . . . 6  class  <. j ,  (/) >.
98cs1 11711 . . . . 5  class  <" <. j ,  (/) >. ">
10 cefg 15330 . . . . . 6  class ~FG
115, 10cfv 5446 . . . . 5  class  ( ~FG  `  i
)
129, 11cec 6895 . . . 4  class  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i )
134, 5, 12cmpt 4258 . . 3  class  ( j  e.  i  |->  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i ) )
142, 3, 13cmpt 4258 . 2  class  ( i  e.  _V  |->  ( j  e.  i  |->  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
151, 14wceq 1652 1  wff varFGrp  =  ( i  e. 
_V  |->  ( j  e.  i  |->  [ <" <. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
Colors of variables: wff set class
This definition is referenced by:  vrgpfval  15390
  Copyright terms: Public domain W3C validator