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