Metamath Proof Explorer

Theorem vrgpf

Description: The mapping from the index set to the generators is a function into the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses vrgpfval.r 
|- .~ = ( ~FG ` I )
vrgpfval.u 
|- U = ( varFGrp ` I )
vrgpf.m 
|- G = ( freeGrp ` I )
vrgpf.x 
|- X = ( Base ` G )
Assertion vrgpf 
|- ( I e. V -> U : I --> X )

Proof

Step Hyp Ref Expression
1 vrgpfval.r 
 |-  .~ = ( ~FG ` I )
2 vrgpfval.u 
 |-  U = ( varFGrp ` I )
3 vrgpf.m 
 |-  G = ( freeGrp ` I )
4 vrgpf.x 
 |-  X = ( Base ` G )
5 1 2 vrgpfval 
 |-  ( I e. V -> U = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
6 0ex 
 |-  (/) e. _V
7 6 prid1 
 |-  (/) e. { (/) , 1o }
8 df2o3 
 |-  2o = { (/) , 1o }
9 7 8 eleqtrri 
 |-  (/) e. 2o
10 opelxpi 
 |-  ( ( j e. I /\ (/) e. 2o ) -> <. j , (/) >. e. ( I X. 2o ) )
11 9 10 mpan2 
 |-  ( j e. I -> <. j , (/) >. e. ( I X. 2o ) )
12 11 adantl 
 |-  ( ( I e. V /\ j e. I ) -> <. j , (/) >. e. ( I X. 2o ) )
13 12 s1cld 
 |-  ( ( I e. V /\ j e. I ) -> <" <. j , (/) >. "> e. Word ( I X. 2o ) )
14 2on 
 |-  2o e. On
15 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
16 14 15 mpan2 
 |-  ( I e. V -> ( I X. 2o ) e. _V )
17 16 adantr 
 |-  ( ( I e. V /\ j e. I ) -> ( I X. 2o ) e. _V )
18 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
19 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
20 17 18 19 3syl 
 |-  ( ( I e. V /\ j e. I ) -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
21 13 20 eleqtrrd 
 |-  ( ( I e. V /\ j e. I ) -> <" <. j , (/) >. "> e. ( _I ` Word ( I X. 2o ) ) )
22 eqid 
 |-  ( _I ` Word ( I X. 2o ) ) = ( _I ` Word ( I X. 2o ) )
23 3 1 22 4 frgpeccl 
 |-  ( <" <. j , (/) >. "> e. ( _I ` Word ( I X. 2o ) ) -> [ <" <. j , (/) >. "> ] .~ e. X )
24 21 23 syl 
 |-  ( ( I e. V /\ j e. I ) -> [ <" <. j , (/) >. "> ] .~ e. X )
25 5 24 fmpt3d 
 |-  ( I e. V -> U : I --> X )