Metamath Proof Explorer

Theorem efgval

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
Assertion efgval 
|- .~ = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 vex 
 |-  i e. _V
4 2on 
 |-  2o e. On
5 4 elexi 
 |-  2o e. _V
6 3 5 xpex 
 |-  ( i X. 2o ) e. _V
7 wrdexg 
 |-  ( ( i X. 2o ) e. _V -> Word ( i X. 2o ) e. _V )
8 fvi 
 |-  ( Word ( i X. 2o ) e. _V -> ( _I ` Word ( i X. 2o ) ) = Word ( i X. 2o ) )
9 6 7 8 mp2b 
 |-  ( _I ` Word ( i X. 2o ) ) = Word ( i X. 2o )
10 xpeq1 
 |-  ( i = I -> ( i X. 2o ) = ( I X. 2o ) )
11 wrdeq 
 |-  ( ( i X. 2o ) = ( I X. 2o ) -> Word ( i X. 2o ) = Word ( I X. 2o ) )
12 10 11 syl 
 |-  ( i = I -> Word ( i X. 2o ) = Word ( I X. 2o ) )
13 12 fveq2d 
 |-  ( i = I -> ( _I ` Word ( i X. 2o ) ) = ( _I ` Word ( I X. 2o ) ) )
14 9 13 eqtr3id 
 |-  ( i = I -> Word ( i X. 2o ) = ( _I ` Word ( I X. 2o ) ) )
15 14 1 eqtr4di 
 |-  ( i = I -> Word ( i X. 2o ) = W )
16 ereq2 
 |-  ( Word ( i X. 2o ) = W -> ( r Er Word ( i X. 2o ) <-> r Er W ) )
17 15 16 syl 
 |-  ( i = I -> ( r Er Word ( i X. 2o ) <-> r Er W ) )
18 raleq 
 |-  ( i = I -> ( A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) )
19 18 ralbidv 
 |-  ( i = I -> ( A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) )
20 15 19 raleqbidv 
 |-  ( i = I -> ( A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) )
21 17 20 anbi12d 
 |-  ( i = I -> ( ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) <-> ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) ) )
22 21 abbidv 
 |-  ( i = I -> { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } = { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
23 22 inteqd 
 |-  ( i = I -> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
24 df-efg 
 |-  ~FG = ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
25 1 efglem 
 |-  E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) )
26 intexab 
 |-  ( E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) <-> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } e. _V )
27 25 26 mpbi 
 |-  |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } e. _V
28 23 24 27 fvmpt 
 |-  ( I e. _V -> ( ~FG ` I ) = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
29 fvprc 
 |-  ( -. I e. _V -> ( ~FG ` I ) = (/) )
30 abn0 
 |-  ( { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } =/= (/) <-> E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) )
31 25 30 mpbir 
 |-  { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } =/= (/)
32 intssuni 
 |-  ( { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } =/= (/) -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ U. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
33 31 32 ax-mp 
 |-  |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ U. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }
34 erssxp 
 |-  ( r Er W -> r C_ ( W X. W ) )
35 1 efgrcl 
 |-  ( x e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
36 35 simpld 
 |-  ( x e. W -> I e. _V )
37 36 con3i 
 |-  ( -. I e. _V -> -. x e. W )
38 37 eq0rdv 
 |-  ( -. I e. _V -> W = (/) )
39 38 xpeq2d 
 |-  ( -. I e. _V -> ( W X. W ) = ( W X. (/) ) )
40 xp0 
 |-  ( W X. (/) ) = (/)
41 39 40 eqtrdi 
 |-  ( -. I e. _V -> ( W X. W ) = (/) )
42 ss0b 
 |-  ( ( W X. W ) C_ (/) <-> ( W X. W ) = (/) )
43 41 42 sylibr 
 |-  ( -. I e. _V -> ( W X. W ) C_ (/) )
44 34 43 sylan9ssr 
 |-  ( ( -. I e. _V /\ r Er W ) -> r C_ (/) )
45 44 ex 
 |-  ( -. I e. _V -> ( r Er W -> r C_ (/) ) )
46 45 adantrd 
 |-  ( -. I e. _V -> ( ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) -> r C_ (/) ) )
47 46 alrimiv 
 |-  ( -. I e. _V -> A. r ( ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) -> r C_ (/) ) )
48 sseq1 
 |-  ( w = r -> ( w C_ (/) <-> r C_ (/) ) )
49 48 ralab2 
 |-  ( A. w e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } w C_ (/) <-> A. r ( ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) -> r C_ (/) ) )
50 47 49 sylibr 
 |-  ( -. I e. _V -> A. w e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } w C_ (/) )
51 unissb 
 |-  ( U. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ (/) <-> A. w e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } w C_ (/) )
52 50 51 sylibr 
 |-  ( -. I e. _V -> U. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ (/) )
53 33 52 sstrid 
 |-  ( -. I e. _V -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ (/) )
54 ss0 
 |-  ( |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } C_ (/) -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } = (/) )
55 53 54 syl 
 |-  ( -. I e. _V -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } = (/) )
56 29 55 eqtr4d 
 |-  ( -. I e. _V -> ( ~FG ` I ) = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
57 28 56 pm2.61i 
 |-  ( ~FG ` I ) = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }
58 2 57 eqtri 
 |-  .~ = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }