Metamath Proof Explorer

Theorem efgi2

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 )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
Assertion efgi2 
|- ( ( A e. W /\ B e. ran ( T ` A ) ) -> A .~ B )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 fveq2 
 |-  ( a = A -> ( T ` a ) = ( T ` A ) )
6 5 rneqd 
 |-  ( a = A -> ran ( T ` a ) = ran ( T ` A ) )
7 eceq1 
 |-  ( a = A -> [ a ] r = [ A ] r )
8 6 7 sseq12d 
 |-  ( a = A -> ( ran ( T ` a ) C_ [ a ] r <-> ran ( T ` A ) C_ [ A ] r ) )
9 8 rspcv 
 |-  ( A e. W -> ( A. a e. W ran ( T ` a ) C_ [ a ] r -> ran ( T ` A ) C_ [ A ] r ) )
10 9 adantr 
 |-  ( ( A e. W /\ B e. ran ( T ` A ) ) -> ( A. a e. W ran ( T ` a ) C_ [ a ] r -> ran ( T ` A ) C_ [ A ] r ) )
11 ssel 
 |-  ( ran ( T ` A ) C_ [ A ] r -> ( B e. ran ( T ` A ) -> B e. [ A ] r ) )
12 11 com12 
 |-  ( B e. ran ( T ` A ) -> ( ran ( T ` A ) C_ [ A ] r -> B e. [ A ] r ) )
13 simpl 
 |-  ( ( B e. [ A ] r /\ A e. W ) -> B e. [ A ] r )
14 elecg 
 |-  ( ( B e. [ A ] r /\ A e. W ) -> ( B e. [ A ] r <-> A r B ) )
15 13 14 mpbid 
 |-  ( ( B e. [ A ] r /\ A e. W ) -> A r B )
16 df-br 
 |-  ( A r B <-> <. A , B >. e. r )
17 15 16 sylib 
 |-  ( ( B e. [ A ] r /\ A e. W ) -> <. A , B >. e. r )
18 17 expcom 
 |-  ( A e. W -> ( B e. [ A ] r -> <. A , B >. e. r ) )
19 12 18 sylan9r 
 |-  ( ( A e. W /\ B e. ran ( T ` A ) ) -> ( ran ( T ` A ) C_ [ A ] r -> <. A , B >. e. r ) )
20 10 19 syld 
 |-  ( ( A e. W /\ B e. ran ( T ` A ) ) -> ( A. a e. W ran ( T ` a ) C_ [ a ] r -> <. A , B >. e. r ) )
21 20 adantld 
 |-  ( ( A e. W /\ B e. ran ( T ` A ) ) -> ( ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) -> <. A , B >. e. r ) )
22 21 alrimiv 
 |-  ( ( A e. W /\ B e. ran ( T ` A ) ) -> A. r ( ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) -> <. A , B >. e. r ) )
23 opex 
 |-  <. A , B >. e. _V
24 23 elintab 
 |-  ( <. A , B >. e. |^| { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) } <-> A. r ( ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) -> <. A , B >. e. r ) )
25 22 24 sylibr 
 |-  ( ( A e. W /\ B e. ran ( T ` A ) ) -> <. A , B >. e. |^| { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) } )
26 1 2 3 4 efgval2 
 |-  .~ = |^| { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) }
27 25 26 eleqtrrdi 
 |-  ( ( A e. W /\ B e. ran ( T ` A ) ) -> <. A , B >. e. .~ )
28 df-br 
 |-  ( A .~ B <-> <. A , B >. e. .~ )
29 27 28 sylibr 
 |-  ( ( A e. W /\ B e. ran ( T ` A ) ) -> A .~ B )