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

Definition df-vrgp 16928
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 16925 . 2  class varFGrp
2 vi . . 3  setvar  i
3 cvv 3106 . . 3  class  _V
4 vj . . . 4  setvar  j
52cv 1397 . . . 4  class  i
64cv 1397 . . . . . . 7  class  j
7 c0 3783 . . . . . . 7  class  (/)
86, 7cop 4022 . . . . . 6  class  <. j ,  (/) >.
98cs1 12521 . . . . 5  class  <" <. j ,  (/) >. ">
10 cefg 16923 . . . . . 6  class ~FG
115, 10cfv 5570 . . . . 5  class  ( ~FG  `  i
)
129, 11cec 7301 . . . 4  class  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i )
134, 5, 12cmpt 4497 . . 3  class  ( j  e.  i  |->  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i ) )
142, 3, 13cmpt 4497 . 2  class  ( i  e.  _V  |->  ( j  e.  i  |->  [ <"
<. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
151, 14wceq 1398 1  wff varFGrp  =  ( i  e. 
_V  |->  ( j  e.  i  |->  [ <" <. j ,  (/) >. "> ] ( ~FG  `  i ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  vrgpfval  16983
  Copyright terms: Public domain W3C validator