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 ) >. "> >. ) ) }