Metamath Proof Explorer

Theorem efgrelexlemb

Description: If two words A , B are related under the free group equivalence, then there exist two extension sequences a , b such that a ends at A , b ends at B , and a and B have the same starting point. (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 ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
efgred.s 
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
efgrelexlem.1 
|- L = { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) }
Assertion efgrelexlemb 
|- .~ C_ L

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 efgred.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
6 efgred.s 
 |-  S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
7 efgrelexlem.1 
 |-  L = { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) }
8 1 2 3 4 efgval2 
 |-  .~ = |^| { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) }
9 7 relopabiv 
 |-  Rel L
10 9 a1i 
 |-  ( T. -> Rel L )
11 simpr 
 |-  ( ( T. /\ f L g ) -> f L g )
12 eqcom 
 |-  ( ( a ` 0 ) = ( b ` 0 ) <-> ( b ` 0 ) = ( a ` 0 ) )
13 12 2rexbii 
 |-  ( E. a e. ( `' S " { f } ) E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) <-> E. a e. ( `' S " { f } ) E. b e. ( `' S " { g } ) ( b ` 0 ) = ( a ` 0 ) )
14 rexcom 
 |-  ( E. a e. ( `' S " { f } ) E. b e. ( `' S " { g } ) ( b ` 0 ) = ( a ` 0 ) <-> E. b e. ( `' S " { g } ) E. a e. ( `' S " { f } ) ( b ` 0 ) = ( a ` 0 ) )
15 13 14 bitri 
 |-  ( E. a e. ( `' S " { f } ) E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) <-> E. b e. ( `' S " { g } ) E. a e. ( `' S " { f } ) ( b ` 0 ) = ( a ` 0 ) )
16 1 2 3 4 5 6 7 efgrelexlema 
 |-  ( f L g <-> E. a e. ( `' S " { f } ) E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) )
17 1 2 3 4 5 6 7 efgrelexlema 
 |-  ( g L f <-> E. b e. ( `' S " { g } ) E. a e. ( `' S " { f } ) ( b ` 0 ) = ( a ` 0 ) )
18 15 16 17 3bitr4i 
 |-  ( f L g <-> g L f )
19 11 18 sylib 
 |-  ( ( T. /\ f L g ) -> g L f )
20 1 2 3 4 5 6 7 efgrelexlema 
 |-  ( g L h <-> E. r e. ( `' S " { g } ) E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) )
21 reeanv 
 |-  ( E. a e. ( `' S " { f } ) E. r e. ( `' S " { g } ) ( E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) /\ E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) ) <-> ( E. a e. ( `' S " { f } ) E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) /\ E. r e. ( `' S " { g } ) E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) ) )
22 1 2 3 4 5 6 efgsfo 
 |-  S : dom S -onto-> W
23 fofn 
 |-  ( S : dom S -onto-> W -> S Fn dom S )
24 22 23 ax-mp 
 |-  S Fn dom S
25 fniniseg 
 |-  ( S Fn dom S -> ( r e. ( `' S " { g } ) <-> ( r e. dom S /\ ( S ` r ) = g ) ) )
26 24 25 ax-mp 
 |-  ( r e. ( `' S " { g } ) <-> ( r e. dom S /\ ( S ` r ) = g ) )
27 fniniseg 
 |-  ( S Fn dom S -> ( b e. ( `' S " { g } ) <-> ( b e. dom S /\ ( S ` b ) = g ) ) )
28 24 27 ax-mp 
 |-  ( b e. ( `' S " { g } ) <-> ( b e. dom S /\ ( S ` b ) = g ) )
29 eqtr3 
 |-  ( ( ( S ` r ) = g /\ ( S ` b ) = g ) -> ( S ` r ) = ( S ` b ) )
30 1 2 3 4 5 6 efgred 
 |-  ( ( r e. dom S /\ b e. dom S /\ ( S ` r ) = ( S ` b ) ) -> ( r ` 0 ) = ( b ` 0 ) )
31 30 eqcomd 
 |-  ( ( r e. dom S /\ b e. dom S /\ ( S ` r ) = ( S ` b ) ) -> ( b ` 0 ) = ( r ` 0 ) )
32 31 3expa 
 |-  ( ( ( r e. dom S /\ b e. dom S ) /\ ( S ` r ) = ( S ` b ) ) -> ( b ` 0 ) = ( r ` 0 ) )
33 29 32 sylan2 
 |-  ( ( ( r e. dom S /\ b e. dom S ) /\ ( ( S ` r ) = g /\ ( S ` b ) = g ) ) -> ( b ` 0 ) = ( r ` 0 ) )
34 33 an4s 
 |-  ( ( ( r e. dom S /\ ( S ` r ) = g ) /\ ( b e. dom S /\ ( S ` b ) = g ) ) -> ( b ` 0 ) = ( r ` 0 ) )
35 26 28 34 syl2anb 
 |-  ( ( r e. ( `' S " { g } ) /\ b e. ( `' S " { g } ) ) -> ( b ` 0 ) = ( r ` 0 ) )
36 eqeq2 
 |-  ( ( r ` 0 ) = ( s ` 0 ) -> ( ( b ` 0 ) = ( r ` 0 ) <-> ( b ` 0 ) = ( s ` 0 ) ) )
37 35 36 syl5ibcom 
 |-  ( ( r e. ( `' S " { g } ) /\ b e. ( `' S " { g } ) ) -> ( ( r ` 0 ) = ( s ` 0 ) -> ( b ` 0 ) = ( s ` 0 ) ) )
38 37 reximdv 
 |-  ( ( r e. ( `' S " { g } ) /\ b e. ( `' S " { g } ) ) -> ( E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) -> E. s e. ( `' S " { h } ) ( b ` 0 ) = ( s ` 0 ) ) )
39 eqeq1 
 |-  ( ( a ` 0 ) = ( b ` 0 ) -> ( ( a ` 0 ) = ( s ` 0 ) <-> ( b ` 0 ) = ( s ` 0 ) ) )
40 39 rexbidv 
 |-  ( ( a ` 0 ) = ( b ` 0 ) -> ( E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) <-> E. s e. ( `' S " { h } ) ( b ` 0 ) = ( s ` 0 ) ) )
41 40 imbi2d 
 |-  ( ( a ` 0 ) = ( b ` 0 ) -> ( ( E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) -> E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) ) <-> ( E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) -> E. s e. ( `' S " { h } ) ( b ` 0 ) = ( s ` 0 ) ) ) )
42 38 41 syl5ibrcom 
 |-  ( ( r e. ( `' S " { g } ) /\ b e. ( `' S " { g } ) ) -> ( ( a ` 0 ) = ( b ` 0 ) -> ( E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) -> E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) ) ) )
43 42 rexlimdva 
 |-  ( r e. ( `' S " { g } ) -> ( E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) -> ( E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) -> E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) ) ) )
44 43 impd 
 |-  ( r e. ( `' S " { g } ) -> ( ( E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) /\ E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) ) -> E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) ) )
45 44 rexlimiv 
 |-  ( E. r e. ( `' S " { g } ) ( E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) /\ E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) ) -> E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) )
46 45 reximi 
 |-  ( E. a e. ( `' S " { f } ) E. r e. ( `' S " { g } ) ( E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) /\ E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) ) -> E. a e. ( `' S " { f } ) E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) )
47 21 46 sylbir 
 |-  ( ( E. a e. ( `' S " { f } ) E. b e. ( `' S " { g } ) ( a ` 0 ) = ( b ` 0 ) /\ E. r e. ( `' S " { g } ) E. s e. ( `' S " { h } ) ( r ` 0 ) = ( s ` 0 ) ) -> E. a e. ( `' S " { f } ) E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) )
48 16 20 47 syl2anb 
 |-  ( ( f L g /\ g L h ) -> E. a e. ( `' S " { f } ) E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) )
49 1 2 3 4 5 6 7 efgrelexlema 
 |-  ( f L h <-> E. a e. ( `' S " { f } ) E. s e. ( `' S " { h } ) ( a ` 0 ) = ( s ` 0 ) )
50 48 49 sylibr 
 |-  ( ( f L g /\ g L h ) -> f L h )
51 50 adantl 
 |-  ( ( T. /\ ( f L g /\ g L h ) ) -> f L h )
52 eqid 
 |-  ( a ` 0 ) = ( a ` 0 )
53 fveq1 
 |-  ( b = a -> ( b ` 0 ) = ( a ` 0 ) )
54 53 rspceeqv 
 |-  ( ( a e. ( `' S " { f } ) /\ ( a ` 0 ) = ( a ` 0 ) ) -> E. b e. ( `' S " { f } ) ( a ` 0 ) = ( b ` 0 ) )
55 52 54 mpan2 
 |-  ( a e. ( `' S " { f } ) -> E. b e. ( `' S " { f } ) ( a ` 0 ) = ( b ` 0 ) )
56 55 pm4.71i 
 |-  ( a e. ( `' S " { f } ) <-> ( a e. ( `' S " { f } ) /\ E. b e. ( `' S " { f } ) ( a ` 0 ) = ( b ` 0 ) ) )
57 fniniseg 
 |-  ( S Fn dom S -> ( a e. ( `' S " { f } ) <-> ( a e. dom S /\ ( S ` a ) = f ) ) )
58 24 57 ax-mp 
 |-  ( a e. ( `' S " { f } ) <-> ( a e. dom S /\ ( S ` a ) = f ) )
59 56 58 bitr3i 
 |-  ( ( a e. ( `' S " { f } ) /\ E. b e. ( `' S " { f } ) ( a ` 0 ) = ( b ` 0 ) ) <-> ( a e. dom S /\ ( S ` a ) = f ) )
60 59 rexbii2 
 |-  ( E. a e. ( `' S " { f } ) E. b e. ( `' S " { f } ) ( a ` 0 ) = ( b ` 0 ) <-> E. a e. dom S ( S ` a ) = f )
61 1 2 3 4 5 6 7 efgrelexlema 
 |-  ( f L f <-> E. a e. ( `' S " { f } ) E. b e. ( `' S " { f } ) ( a ` 0 ) = ( b ` 0 ) )
62 forn 
 |-  ( S : dom S -onto-> W -> ran S = W )
63 22 62 ax-mp 
 |-  ran S = W
64 63 eleq2i 
 |-  ( f e. ran S <-> f e. W )
65 fvelrnb 
 |-  ( S Fn dom S -> ( f e. ran S <-> E. a e. dom S ( S ` a ) = f ) )
66 24 65 ax-mp 
 |-  ( f e. ran S <-> E. a e. dom S ( S ` a ) = f )
67 64 66 bitr3i 
 |-  ( f e. W <-> E. a e. dom S ( S ` a ) = f )
68 60 61 67 3bitr4ri 
 |-  ( f e. W <-> f L f )
69 68 a1i 
 |-  ( T. -> ( f e. W <-> f L f ) )
70 10 19 51 69 iserd 
 |-  ( T. -> L Er W )
71 70 mptru 
 |-  L Er W
72 simpl 
 |-  ( ( a e. W /\ b e. ran ( T ` a ) ) -> a e. W )
73 foelrn 
 |-  ( ( S : dom S -onto-> W /\ a e. W ) -> E. r e. dom S a = ( S ` r ) )
74 22 72 73 sylancr 
 |-  ( ( a e. W /\ b e. ran ( T ` a ) ) -> E. r e. dom S a = ( S ` r ) )
75 simprl 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> r e. dom S )
76 simprr 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> a = ( S ` r ) )
77 76 eqcomd 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ( S ` r ) = a )
78 fniniseg 
 |-  ( S Fn dom S -> ( r e. ( `' S " { a } ) <-> ( r e. dom S /\ ( S ` r ) = a ) ) )
79 24 78 ax-mp 
 |-  ( r e. ( `' S " { a } ) <-> ( r e. dom S /\ ( S ` r ) = a ) )
80 75 77 79 sylanbrc 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> r e. ( `' S " { a } ) )
81 simplr 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> b e. ran ( T ` a ) )
82 76 fveq2d 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ( T ` a ) = ( T ` ( S ` r ) ) )
83 82 rneqd 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ran ( T ` a ) = ran ( T ` ( S ` r ) ) )
84 81 83 eleqtrd 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> b e. ran ( T ` ( S ` r ) ) )
85 1 2 3 4 5 6 efgsp1 
 |-  ( ( r e. dom S /\ b e. ran ( T ` ( S ` r ) ) ) -> ( r ++ <" b "> ) e. dom S )
86 75 84 85 syl2anc 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ( r ++ <" b "> ) e. dom S )
87 1 2 3 4 5 6 efgsdm 
 |-  ( r e. dom S <-> ( r e. ( Word W \ { (/) } ) /\ ( r ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` r ) ) ( r ` i ) e. ran ( T ` ( r ` ( i - 1 ) ) ) ) )
88 87 simp1bi 
 |-  ( r e. dom S -> r e. ( Word W \ { (/) } ) )
89 88 ad2antrl 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> r e. ( Word W \ { (/) } ) )
90 89 eldifad 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> r e. Word W )
91 1 2 3 4 efgtf 
 |-  ( a e. W -> ( ( T ` a ) = ( f e. ( 0 ... ( # ` a ) ) , g e. ( I X. 2o ) |-> ( a splice <. f , f , <" g ( M ` g ) "> >. ) ) /\ ( T ` a ) : ( ( 0 ... ( # ` a ) ) X. ( I X. 2o ) ) --> W ) )
92 91 simprd 
 |-  ( a e. W -> ( T ` a ) : ( ( 0 ... ( # ` a ) ) X. ( I X. 2o ) ) --> W )
93 92 frnd 
 |-  ( a e. W -> ran ( T ` a ) C_ W )
94 93 sselda 
 |-  ( ( a e. W /\ b e. ran ( T ` a ) ) -> b e. W )
95 94 adantr 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> b e. W )
96 1 2 3 4 5 6 efgsval2 
 |-  ( ( r e. Word W /\ b e. W /\ ( r ++ <" b "> ) e. dom S ) -> ( S ` ( r ++ <" b "> ) ) = b )
97 90 95 86 96 syl3anc 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ( S ` ( r ++ <" b "> ) ) = b )
98 fniniseg 
 |-  ( S Fn dom S -> ( ( r ++ <" b "> ) e. ( `' S " { b } ) <-> ( ( r ++ <" b "> ) e. dom S /\ ( S ` ( r ++ <" b "> ) ) = b ) ) )
99 24 98 ax-mp 
 |-  ( ( r ++ <" b "> ) e. ( `' S " { b } ) <-> ( ( r ++ <" b "> ) e. dom S /\ ( S ` ( r ++ <" b "> ) ) = b ) )
100 86 97 99 sylanbrc 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ( r ++ <" b "> ) e. ( `' S " { b } ) )
101 95 s1cld 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> <" b "> e. Word W )
102 eldifsn 
 |-  ( r e. ( Word W \ { (/) } ) <-> ( r e. Word W /\ r =/= (/) ) )
103 lennncl 
 |-  ( ( r e. Word W /\ r =/= (/) ) -> ( # ` r ) e. NN )
104 102 103 sylbi 
 |-  ( r e. ( Word W \ { (/) } ) -> ( # ` r ) e. NN )
105 89 104 syl 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ( # ` r ) e. NN )
106 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` r ) ) <-> ( # ` r ) e. NN )
107 105 106 sylibr 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> 0 e. ( 0 ..^ ( # ` r ) ) )
108 ccatval1 
 |-  ( ( r e. Word W /\ <" b "> e. Word W /\ 0 e. ( 0 ..^ ( # ` r ) ) ) -> ( ( r ++ <" b "> ) ` 0 ) = ( r ` 0 ) )
109 90 101 107 108 syl3anc 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ( ( r ++ <" b "> ) ` 0 ) = ( r ` 0 ) )
110 109 eqcomd 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> ( r ` 0 ) = ( ( r ++ <" b "> ) ` 0 ) )
111 fveq1 
 |-  ( s = ( r ++ <" b "> ) -> ( s ` 0 ) = ( ( r ++ <" b "> ) ` 0 ) )
112 111 rspceeqv 
 |-  ( ( ( r ++ <" b "> ) e. ( `' S " { b } ) /\ ( r ` 0 ) = ( ( r ++ <" b "> ) ` 0 ) ) -> E. s e. ( `' S " { b } ) ( r ` 0 ) = ( s ` 0 ) )
113 100 110 112 syl2anc 
 |-  ( ( ( a e. W /\ b e. ran ( T ` a ) ) /\ ( r e. dom S /\ a = ( S ` r ) ) ) -> E. s e. ( `' S " { b } ) ( r ` 0 ) = ( s ` 0 ) )
114 74 80 113 reximssdv 
 |-  ( ( a e. W /\ b e. ran ( T ` a ) ) -> E. r e. ( `' S " { a } ) E. s e. ( `' S " { b } ) ( r ` 0 ) = ( s ` 0 ) )
115 1 2 3 4 5 6 7 efgrelexlema 
 |-  ( a L b <-> E. r e. ( `' S " { a } ) E. s e. ( `' S " { b } ) ( r ` 0 ) = ( s ` 0 ) )
116 114 115 sylibr 
 |-  ( ( a e. W /\ b e. ran ( T ` a ) ) -> a L b )
117 vex 
 |-  b e. _V
118 vex 
 |-  a e. _V
119 117 118 elec 
 |-  ( b e. [ a ] L <-> a L b )
120 116 119 sylibr 
 |-  ( ( a e. W /\ b e. ran ( T ` a ) ) -> b e. [ a ] L )
121 120 ex 
 |-  ( a e. W -> ( b e. ran ( T ` a ) -> b e. [ a ] L ) )
122 121 ssrdv 
 |-  ( a e. W -> ran ( T ` a ) C_ [ a ] L )
123 122 rgen 
 |-  A. a e. W ran ( T ` a ) C_ [ a ] L
124 1 fvexi 
 |-  W e. _V
125 erex 
 |-  ( L Er W -> ( W e. _V -> L e. _V ) )
126 71 124 125 mp2 
 |-  L e. _V
127 ereq1 
 |-  ( r = L -> ( r Er W <-> L Er W ) )
128 eceq2 
 |-  ( r = L -> [ a ] r = [ a ] L )
129 128 sseq2d 
 |-  ( r = L -> ( ran ( T ` a ) C_ [ a ] r <-> ran ( T ` a ) C_ [ a ] L ) )
130 129 ralbidv 
 |-  ( r = L -> ( A. a e. W ran ( T ` a ) C_ [ a ] r <-> A. a e. W ran ( T ` a ) C_ [ a ] L ) )
131 127 130 anbi12d 
 |-  ( r = L -> ( ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) <-> ( L Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] L ) ) )
132 126 131 elab 
 |-  ( L e. { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) } <-> ( L Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] L ) )
133 71 123 132 mpbir2an 
 |-  L e. { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) }
134 intss1 
 |-  ( L e. { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) } -> |^| { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) } C_ L )
135 133 134 ax-mp 
 |-  |^| { r | ( r Er W /\ A. a e. W ran ( T ` a ) C_ [ a ] r ) } C_ L
136 8 135 eqsstri 
 |-  .~ C_ L