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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-vrgp | |- varFGrp = ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cvrgp | |- varFGrp |
|
| 1 | vi | |- i |
|
| 2 | cvv | |- _V |
|
| 3 | vj | |- j |
|
| 4 | 1 | cv | |- i |
| 5 | 3 | cv | |- j |
| 6 | c0 | |- (/) |
|
| 7 | 5 6 | cop | |- <. j , (/) >. |
| 8 | 7 | cs1 | |- <" <. j , (/) >. "> |
| 9 | cefg | |- ~FG |
|
| 10 | 4 9 | cfv | |- ( ~FG ` i ) |
| 11 | 8 10 | cec | |- [ <" <. j , (/) >. "> ] ( ~FG ` i ) |
| 12 | 3 4 11 | cmpt | |- ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) |
| 13 | 1 2 12 | cmpt | |- ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) ) |
| 14 | 0 13 | wceq | |- varFGrp = ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) ) |