Metamath Proof Explorer

Theorem ptrest

Description: Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019)

Ref Expression
Hypotheses ptrest.0 
|- ( ph -> A e. V )
ptrest.1 
|- ( ph -> F : A --> Top )
ptrest.2 
|- ( ( ph /\ k e. A ) -> S e. W )
Assertion ptrest 
|- ( ph -> ( ( Xt_ ` F ) |`t X_ k e. A S ) = ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) )

Proof

Step Hyp Ref Expression
1 ptrest.0 
 |-  ( ph -> A e. V )
2 ptrest.1 
 |-  ( ph -> F : A --> Top )
3 ptrest.2 
 |-  ( ( ph /\ k e. A ) -> S e. W )
4 firest 
 |-  ( fi ` ( ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |`t X_ k e. A S ) ) = ( ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) |`t X_ k e. A S )
5 snex 
 |-  { U. ( Xt_ ` F ) } e. _V
6 fvex 
 |-  ( F ` u ) e. _V
7 6 rgenw 
 |-  A. u e. A ( F ` u ) e. _V
8 eqid 
 |-  ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) = ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) )
9 8 mpoexxg 
 |-  ( ( A e. V /\ A. u e. A ( F ` u ) e. _V ) -> ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) e. _V )
10 1 7 9 sylancl 
 |-  ( ph -> ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) e. _V )
11 rnexg 
 |-  ( ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) e. _V -> ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) e. _V )
12 10 11 syl 
 |-  ( ph -> ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) e. _V )
13 unexg 
 |-  ( ( { U. ( Xt_ ` F ) } e. _V /\ ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) e. _V ) -> ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) e. _V )
14 5 12 13 sylancr 
 |-  ( ph -> ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) e. _V )
15 3 ralrimiva 
 |-  ( ph -> A. k e. A S e. W )
16 ixpexg 
 |-  ( A. k e. A S e. W -> X_ k e. A S e. _V )
17 15 16 syl 
 |-  ( ph -> X_ k e. A S e. _V )
18 restval 
 |-  ( ( ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) e. _V /\ X_ k e. A S e. _V ) -> ( ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |`t X_ k e. A S ) = ran ( x e. ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |-> ( x i^i X_ k e. A S ) ) )
19 14 17 18 syl2anc 
 |-  ( ph -> ( ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |`t X_ k e. A S ) = ran ( x e. ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |-> ( x i^i X_ k e. A S ) ) )
20 mptun 
 |-  ( x e. ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |-> ( x i^i X_ k e. A S ) ) = ( ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) u. ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) )
21 20 rneqi 
 |-  ran ( x e. ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |-> ( x i^i X_ k e. A S ) ) = ran ( ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) u. ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) )
22 rnun 
 |-  ran ( ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) u. ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) ) = ( ran ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) u. ran ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) )
23 21 22 eqtri 
 |-  ran ( x e. ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |-> ( x i^i X_ k e. A S ) ) = ( ran ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) u. ran ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) )
24 elsni 
 |-  ( x e. { U. ( Xt_ ` F ) } -> x = U. ( Xt_ ` F ) )
25 24 ineq1d 
 |-  ( x e. { U. ( Xt_ ` F ) } -> ( x i^i X_ k e. A S ) = ( U. ( Xt_ ` F ) i^i X_ k e. A S ) )
26 25 mpteq2ia 
 |-  ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) = ( x e. { U. ( Xt_ ` F ) } |-> ( U. ( Xt_ ` F ) i^i X_ k e. A S ) )
27 fvex 
 |-  ( Xt_ ` F ) e. _V
28 27 uniex 
 |-  U. ( Xt_ ` F ) e. _V
29 28 inex1 
 |-  ( U. ( Xt_ ` F ) i^i X_ k e. A S ) e. _V
30 fmptsn 
 |-  ( ( U. ( Xt_ ` F ) e. _V /\ ( U. ( Xt_ ` F ) i^i X_ k e. A S ) e. _V ) -> { <. U. ( Xt_ ` F ) , ( U. ( Xt_ ` F ) i^i X_ k e. A S ) >. } = ( x e. { U. ( Xt_ ` F ) } |-> ( U. ( Xt_ ` F ) i^i X_ k e. A S ) ) )
31 28 29 30 mp2an 
 |-  { <. U. ( Xt_ ` F ) , ( U. ( Xt_ ` F ) i^i X_ k e. A S ) >. } = ( x e. { U. ( Xt_ ` F ) } |-> ( U. ( Xt_ ` F ) i^i X_ k e. A S ) )
32 26 31 eqtr4i 
 |-  ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) = { <. U. ( Xt_ ` F ) , ( U. ( Xt_ ` F ) i^i X_ k e. A S ) >. }
33 32 rneqi 
 |-  ran ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) = ran { <. U. ( Xt_ ` F ) , ( U. ( Xt_ ` F ) i^i X_ k e. A S ) >. }
34 28 rnsnop 
 |-  ran { <. U. ( Xt_ ` F ) , ( U. ( Xt_ ` F ) i^i X_ k e. A S ) >. } = { ( U. ( Xt_ ` F ) i^i X_ k e. A S ) }
35 33 34 eqtri 
 |-  ran ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) = { ( U. ( Xt_ ` F ) i^i X_ k e. A S ) }
36 2 ffvelrnda 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. Top )
37 inss1 
 |-  ( U. ( F ` k ) i^i S ) C_ U. ( F ` k )
38 eqid 
 |-  U. ( F ` k ) = U. ( F ` k )
39 38 restuni 
 |-  ( ( ( F ` k ) e. Top /\ ( U. ( F ` k ) i^i S ) C_ U. ( F ` k ) ) -> ( U. ( F ` k ) i^i S ) = U. ( ( F ` k ) |`t ( U. ( F ` k ) i^i S ) ) )
40 36 37 39 sylancl 
 |-  ( ( ph /\ k e. A ) -> ( U. ( F ` k ) i^i S ) = U. ( ( F ` k ) |`t ( U. ( F ` k ) i^i S ) ) )
41 fvex 
 |-  ( F ` k ) e. _V
42 38 restin 
 |-  ( ( ( F ` k ) e. _V /\ S e. W ) -> ( ( F ` k ) |`t S ) = ( ( F ` k ) |`t ( S i^i U. ( F ` k ) ) ) )
43 41 3 42 sylancr 
 |-  ( ( ph /\ k e. A ) -> ( ( F ` k ) |`t S ) = ( ( F ` k ) |`t ( S i^i U. ( F ` k ) ) ) )
44 incom 
 |-  ( S i^i U. ( F ` k ) ) = ( U. ( F ` k ) i^i S )
45 44 oveq2i 
 |-  ( ( F ` k ) |`t ( S i^i U. ( F ` k ) ) ) = ( ( F ` k ) |`t ( U. ( F ` k ) i^i S ) )
46 43 45 eqtrdi 
 |-  ( ( ph /\ k e. A ) -> ( ( F ` k ) |`t S ) = ( ( F ` k ) |`t ( U. ( F ` k ) i^i S ) ) )
47 46 unieqd 
 |-  ( ( ph /\ k e. A ) -> U. ( ( F ` k ) |`t S ) = U. ( ( F ` k ) |`t ( U. ( F ` k ) i^i S ) ) )
48 40 47 eqtr4d 
 |-  ( ( ph /\ k e. A ) -> ( U. ( F ` k ) i^i S ) = U. ( ( F ` k ) |`t S ) )
49 48 ixpeq2dva 
 |-  ( ph -> X_ k e. A ( U. ( F ` k ) i^i S ) = X_ k e. A U. ( ( F ` k ) |`t S ) )
50 ixpin 
 |-  X_ k e. A ( U. ( F ` k ) i^i S ) = ( X_ k e. A U. ( F ` k ) i^i X_ k e. A S )
51 nfcv 
 |-  F/_ y U. ( ( F ` k ) |`t S )
52 nfcv 
 |-  F/_ k ( F ` y )
53 nfcv 
 |-  F/_ k |`t
54 nfcsb1v 
 |-  F/_ k [_ y / k ]_ S
55 52 53 54 nfov 
 |-  F/_ k ( ( F ` y ) |`t [_ y / k ]_ S )
56 55 nfuni 
 |-  F/_ k U. ( ( F ` y ) |`t [_ y / k ]_ S )
57 fveq2 
 |-  ( k = y -> ( F ` k ) = ( F ` y ) )
58 csbeq1a 
 |-  ( k = y -> S = [_ y / k ]_ S )
59 57 58 oveq12d 
 |-  ( k = y -> ( ( F ` k ) |`t S ) = ( ( F ` y ) |`t [_ y / k ]_ S ) )
60 59 unieqd 
 |-  ( k = y -> U. ( ( F ` k ) |`t S ) = U. ( ( F ` y ) |`t [_ y / k ]_ S ) )
61 51 56 60 cbvixp 
 |-  X_ k e. A U. ( ( F ` k ) |`t S ) = X_ y e. A U. ( ( F ` y ) |`t [_ y / k ]_ S )
62 ixpeq2 
 |-  ( A. y e. A U. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) = U. ( ( F ` y ) |`t [_ y / k ]_ S ) -> X_ y e. A U. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) = X_ y e. A U. ( ( F ` y ) |`t [_ y / k ]_ S ) )
63 ovex 
 |-  ( ( F ` y ) |`t [_ y / k ]_ S ) e. _V
64 nfcv 
 |-  F/_ k y
65 eqid 
 |-  ( k e. A |-> ( ( F ` k ) |`t S ) ) = ( k e. A |-> ( ( F ` k ) |`t S ) )
66 64 55 59 65 fvmptf 
 |-  ( ( y e. A /\ ( ( F ` y ) |`t [_ y / k ]_ S ) e. _V ) -> ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) = ( ( F ` y ) |`t [_ y / k ]_ S ) )
67 63 66 mpan2 
 |-  ( y e. A -> ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) = ( ( F ` y ) |`t [_ y / k ]_ S ) )
68 67 unieqd 
 |-  ( y e. A -> U. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) = U. ( ( F ` y ) |`t [_ y / k ]_ S ) )
69 62 68 mprg 
 |-  X_ y e. A U. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) = X_ y e. A U. ( ( F ` y ) |`t [_ y / k ]_ S )
70 61 69 eqtr4i 
 |-  X_ k e. A U. ( ( F ` k ) |`t S ) = X_ y e. A U. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y )
71 49 50 70 3eqtr3g 
 |-  ( ph -> ( X_ k e. A U. ( F ` k ) i^i X_ k e. A S ) = X_ y e. A U. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) )
72 eqid 
 |-  ( Xt_ ` F ) = ( Xt_ ` F )
73 72 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. ( Xt_ ` F ) )
74 1 2 73 syl2anc 
 |-  ( ph -> X_ k e. A U. ( F ` k ) = U. ( Xt_ ` F ) )
75 74 ineq1d 
 |-  ( ph -> ( X_ k e. A U. ( F ` k ) i^i X_ k e. A S ) = ( U. ( Xt_ ` F ) i^i X_ k e. A S ) )
76 resttop 
 |-  ( ( ( F ` k ) e. Top /\ S e. W ) -> ( ( F ` k ) |`t S ) e. Top )
77 36 3 76 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( F ` k ) |`t S ) e. Top )
78 77 fmpttd 
 |-  ( ph -> ( k e. A |-> ( ( F ` k ) |`t S ) ) : A --> Top )
79 eqid 
 |-  ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) = ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) )
80 79 ptuni 
 |-  ( ( A e. V /\ ( k e. A |-> ( ( F ` k ) |`t S ) ) : A --> Top ) -> X_ y e. A U. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) = U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) )
81 1 78 80 syl2anc 
 |-  ( ph -> X_ y e. A U. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` y ) = U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) )
82 71 75 81 3eqtr3d 
 |-  ( ph -> ( U. ( Xt_ ` F ) i^i X_ k e. A S ) = U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) )
83 82 sneqd 
 |-  ( ph -> { ( U. ( Xt_ ` F ) i^i X_ k e. A S ) } = { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } )
84 35 83 syl5eq 
 |-  ( ph -> ran ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) = { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } )
85 vex 
 |-  w e. _V
86 85 elixp 
 |-  ( w e. X_ k e. A S <-> ( w Fn A /\ A. k e. A ( w ` k ) e. S ) )
87 86 simprbi 
 |-  ( w e. X_ k e. A S -> A. k e. A ( w ` k ) e. S )
88 nfcsb1v 
 |-  F/_ k [_ u / k ]_ S
89 88 nfel2 
 |-  F/ k ( w ` u ) e. [_ u / k ]_ S
90 fveq2 
 |-  ( k = u -> ( w ` k ) = ( w ` u ) )
91 csbeq1a 
 |-  ( k = u -> S = [_ u / k ]_ S )
92 90 91 eleq12d 
 |-  ( k = u -> ( ( w ` k ) e. S <-> ( w ` u ) e. [_ u / k ]_ S ) )
93 89 92 rspc 
 |-  ( u e. A -> ( A. k e. A ( w ` k ) e. S -> ( w ` u ) e. [_ u / k ]_ S ) )
94 87 93 syl5 
 |-  ( u e. A -> ( w e. X_ k e. A S -> ( w ` u ) e. [_ u / k ]_ S ) )
95 94 pm4.71d 
 |-  ( u e. A -> ( w e. X_ k e. A S <-> ( w e. X_ k e. A S /\ ( w ` u ) e. [_ u / k ]_ S ) ) )
96 95 anbi2d 
 |-  ( u e. A -> ( ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ w e. X_ k e. A S ) <-> ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ ( w e. X_ k e. A S /\ ( w ` u ) e. [_ u / k ]_ S ) ) ) )
97 an4 
 |-  ( ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ ( w e. X_ k e. A S /\ ( w ` u ) e. [_ u / k ]_ S ) ) <-> ( ( w e. U. ( Xt_ ` F ) /\ w e. X_ k e. A S ) /\ ( ( w ` u ) e. v /\ ( w ` u ) e. [_ u / k ]_ S ) ) )
98 elin 
 |-  ( ( w ` u ) e. ( v i^i [_ u / k ]_ S ) <-> ( ( w ` u ) e. v /\ ( w ` u ) e. [_ u / k ]_ S ) )
99 98 anbi2i 
 |-  ( ( ( w e. U. ( Xt_ ` F ) /\ w e. X_ k e. A S ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) <-> ( ( w e. U. ( Xt_ ` F ) /\ w e. X_ k e. A S ) /\ ( ( w ` u ) e. v /\ ( w ` u ) e. [_ u / k ]_ S ) ) )
100 97 99 bitr4i 
 |-  ( ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ ( w e. X_ k e. A S /\ ( w ` u ) e. [_ u / k ]_ S ) ) <-> ( ( w e. U. ( Xt_ ` F ) /\ w e. X_ k e. A S ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) )
101 96 100 bitrdi 
 |-  ( u e. A -> ( ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ w e. X_ k e. A S ) <-> ( ( w e. U. ( Xt_ ` F ) /\ w e. X_ k e. A S ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) ) )
102 elin 
 |-  ( w e. ( U. ( Xt_ ` F ) i^i X_ k e. A S ) <-> ( w e. U. ( Xt_ ` F ) /\ w e. X_ k e. A S ) )
103 82 eleq2d 
 |-  ( ph -> ( w e. ( U. ( Xt_ ` F ) i^i X_ k e. A S ) <-> w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) ) )
104 102 103 bitr3id 
 |-  ( ph -> ( ( w e. U. ( Xt_ ` F ) /\ w e. X_ k e. A S ) <-> w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) ) )
105 104 anbi1d 
 |-  ( ph -> ( ( ( w e. U. ( Xt_ ` F ) /\ w e. X_ k e. A S ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) <-> ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) ) )
106 101 105 sylan9bbr 
 |-  ( ( ph /\ u e. A ) -> ( ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ w e. X_ k e. A S ) <-> ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) ) )
107 106 abbidv 
 |-  ( ( ph /\ u e. A ) -> { w | ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ w e. X_ k e. A S ) } = { w | ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) } )
108 eqid 
 |-  ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) = ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) )
109 108 mptpreima 
 |-  ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) = { w e. U. ( Xt_ ` F ) | ( w ` u ) e. v }
110 df-rab 
 |-  { w e. U. ( Xt_ ` F ) | ( w ` u ) e. v } = { w | ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) }
111 109 110 eqtr2i 
 |-  { w | ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) } = ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v )
112 abid2 
 |-  { w | w e. X_ k e. A S } = X_ k e. A S
113 111 112 ineq12i 
 |-  ( { w | ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) } i^i { w | w e. X_ k e. A S } ) = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S )
114 inab 
 |-  ( { w | ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) } i^i { w | w e. X_ k e. A S } ) = { w | ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ w e. X_ k e. A S ) }
115 113 114 eqtr3i 
 |-  ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) = { w | ( ( w e. U. ( Xt_ ` F ) /\ ( w ` u ) e. v ) /\ w e. X_ k e. A S ) }
116 eqid 
 |-  ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) = ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) )
117 116 mptpreima 
 |-  ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( v i^i [_ u / k ]_ S ) ) = { w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) | ( w ` u ) e. ( v i^i [_ u / k ]_ S ) }
118 df-rab 
 |-  { w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) | ( w ` u ) e. ( v i^i [_ u / k ]_ S ) } = { w | ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) }
119 117 118 eqtri 
 |-  ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( v i^i [_ u / k ]_ S ) ) = { w | ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) /\ ( w ` u ) e. ( v i^i [_ u / k ]_ S ) ) }
120 107 115 119 3eqtr4g 
 |-  ( ( ph /\ u e. A ) -> ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( v i^i [_ u / k ]_ S ) ) )
121 120 eqeq2d 
 |-  ( ( ph /\ u e. A ) -> ( x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) <-> x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( v i^i [_ u / k ]_ S ) ) ) )
122 121 rexbidv 
 |-  ( ( ph /\ u e. A ) -> ( E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) <-> E. v e. ( F ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( v i^i [_ u / k ]_ S ) ) ) )
123 ineq1 
 |-  ( v = y -> ( v i^i [_ u / k ]_ S ) = ( y i^i [_ u / k ]_ S ) )
124 123 imaeq2d 
 |-  ( v = y -> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( v i^i [_ u / k ]_ S ) ) = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( y i^i [_ u / k ]_ S ) ) )
125 124 eqeq2d 
 |-  ( v = y -> ( x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( v i^i [_ u / k ]_ S ) ) <-> x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( y i^i [_ u / k ]_ S ) ) ) )
126 125 cbvrexvw 
 |-  ( E. v e. ( F ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( v i^i [_ u / k ]_ S ) ) <-> E. y e. ( F ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( y i^i [_ u / k ]_ S ) ) )
127 122 126 bitrdi 
 |-  ( ( ph /\ u e. A ) -> ( E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) <-> E. y e. ( F ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( y i^i [_ u / k ]_ S ) ) ) )
128 vex 
 |-  y e. _V
129 128 inex1 
 |-  ( y i^i [_ u / k ]_ S ) e. _V
130 129 a1i 
 |-  ( ( ( ph /\ u e. A ) /\ y e. ( F ` u ) ) -> ( y i^i [_ u / k ]_ S ) e. _V )
131 ovex 
 |-  ( ( F ` u ) |`t [_ u / k ]_ S ) e. _V
132 nfcv 
 |-  F/_ k u
133 nfcv 
 |-  F/_ k ( F ` u )
134 133 53 88 nfov 
 |-  F/_ k ( ( F ` u ) |`t [_ u / k ]_ S )
135 fveq2 
 |-  ( k = u -> ( F ` k ) = ( F ` u ) )
136 135 91 oveq12d 
 |-  ( k = u -> ( ( F ` k ) |`t S ) = ( ( F ` u ) |`t [_ u / k ]_ S ) )
137 132 134 136 65 fvmptf 
 |-  ( ( u e. A /\ ( ( F ` u ) |`t [_ u / k ]_ S ) e. _V ) -> ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) = ( ( F ` u ) |`t [_ u / k ]_ S ) )
138 131 137 mpan2 
 |-  ( u e. A -> ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) = ( ( F ` u ) |`t [_ u / k ]_ S ) )
139 138 adantl 
 |-  ( ( ph /\ u e. A ) -> ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) = ( ( F ` u ) |`t [_ u / k ]_ S ) )
140 139 eleq2d 
 |-  ( ( ph /\ u e. A ) -> ( v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) <-> v e. ( ( F ` u ) |`t [_ u / k ]_ S ) ) )
141 nfv 
 |-  F/ k ( ph /\ u e. A )
142 nfcsb1v 
 |-  F/_ k [_ u / k ]_ W
143 88 142 nfel 
 |-  F/ k [_ u / k ]_ S e. [_ u / k ]_ W
144 141 143 nfim 
 |-  F/ k ( ( ph /\ u e. A ) -> [_ u / k ]_ S e. [_ u / k ]_ W )
145 eleq1w 
 |-  ( k = u -> ( k e. A <-> u e. A ) )
146 145 anbi2d 
 |-  ( k = u -> ( ( ph /\ k e. A ) <-> ( ph /\ u e. A ) ) )
147 csbeq1a 
 |-  ( k = u -> W = [_ u / k ]_ W )
148 91 147 eleq12d 
 |-  ( k = u -> ( S e. W <-> [_ u / k ]_ S e. [_ u / k ]_ W ) )
149 146 148 imbi12d 
 |-  ( k = u -> ( ( ( ph /\ k e. A ) -> S e. W ) <-> ( ( ph /\ u e. A ) -> [_ u / k ]_ S e. [_ u / k ]_ W ) ) )
150 144 149 3 chvarfv 
 |-  ( ( ph /\ u e. A ) -> [_ u / k ]_ S e. [_ u / k ]_ W )
151 elrest 
 |-  ( ( ( F ` u ) e. _V /\ [_ u / k ]_ S e. [_ u / k ]_ W ) -> ( v e. ( ( F ` u ) |`t [_ u / k ]_ S ) <-> E. y e. ( F ` u ) v = ( y i^i [_ u / k ]_ S ) ) )
152 6 150 151 sylancr 
 |-  ( ( ph /\ u e. A ) -> ( v e. ( ( F ` u ) |`t [_ u / k ]_ S ) <-> E. y e. ( F ` u ) v = ( y i^i [_ u / k ]_ S ) ) )
153 140 152 bitrd 
 |-  ( ( ph /\ u e. A ) -> ( v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) <-> E. y e. ( F ` u ) v = ( y i^i [_ u / k ]_ S ) ) )
154 imaeq2 
 |-  ( v = ( y i^i [_ u / k ]_ S ) -> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( y i^i [_ u / k ]_ S ) ) )
155 154 eqeq2d 
 |-  ( v = ( y i^i [_ u / k ]_ S ) -> ( x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) <-> x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( y i^i [_ u / k ]_ S ) ) ) )
156 155 adantl 
 |-  ( ( ( ph /\ u e. A ) /\ v = ( y i^i [_ u / k ]_ S ) ) -> ( x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) <-> x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( y i^i [_ u / k ]_ S ) ) ) )
157 130 153 156 rexxfr2d 
 |-  ( ( ph /\ u e. A ) -> ( E. v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) <-> E. y e. ( F ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " ( y i^i [_ u / k ]_ S ) ) ) )
158 127 157 bitr4d 
 |-  ( ( ph /\ u e. A ) -> ( E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) <-> E. v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) )
159 158 rexbidva 
 |-  ( ph -> ( E. u e. A E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) <-> E. u e. A E. v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) )
160 159 abbidv 
 |-  ( ph -> { x | E. u e. A E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) } = { x | E. u e. A E. v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) } )
161 eqid 
 |-  ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) = ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) )
162 161 rnmpt 
 |-  ran ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) = { y | E. x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) y = ( x i^i X_ k e. A S ) }
163 nfre1 
 |-  F/ x E. x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) y = ( x i^i X_ k e. A S )
164 nfv 
 |-  F/ y E. u e. A E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S )
165 28 mptex 
 |-  ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) e. _V
166 165 cnvex 
 |-  `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) e. _V
167 166 imaex 
 |-  ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) e. _V
168 167 rgen2w 
 |-  A. u e. A A. v e. ( F ` u ) ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) e. _V
169 ineq1 
 |-  ( x = ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) -> ( x i^i X_ k e. A S ) = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) )
170 169 eqeq2d 
 |-  ( x = ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) -> ( y = ( x i^i X_ k e. A S ) <-> y = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) ) )
171 8 170 rexrnmpo 
 |-  ( A. u e. A A. v e. ( F ` u ) ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) e. _V -> ( E. x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) y = ( x i^i X_ k e. A S ) <-> E. u e. A E. v e. ( F ` u ) y = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) ) )
172 168 171 ax-mp 
 |-  ( E. x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) y = ( x i^i X_ k e. A S ) <-> E. u e. A E. v e. ( F ` u ) y = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) )
173 eqeq1 
 |-  ( y = x -> ( y = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) <-> x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) ) )
174 173 2rexbidv 
 |-  ( y = x -> ( E. u e. A E. v e. ( F ` u ) y = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) <-> E. u e. A E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) ) )
175 172 174 syl5bb 
 |-  ( y = x -> ( E. x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) y = ( x i^i X_ k e. A S ) <-> E. u e. A E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) ) )
176 163 164 175 cbvabw 
 |-  { y | E. x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) y = ( x i^i X_ k e. A S ) } = { x | E. u e. A E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) }
177 162 176 eqtri 
 |-  ran ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) = { x | E. u e. A E. v e. ( F ` u ) x = ( ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) i^i X_ k e. A S ) }
178 eqid 
 |-  ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) = ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) )
179 178 rnmpo 
 |-  ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) = { x | E. u e. A E. v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) x = ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) }
180 160 177 179 3eqtr4g 
 |-  ( ph -> ran ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) = ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) )
181 84 180 uneq12d 
 |-  ( ph -> ( ran ( x e. { U. ( Xt_ ` F ) } |-> ( x i^i X_ k e. A S ) ) u. ran ( x e. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) |-> ( x i^i X_ k e. A S ) ) ) = ( { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } u. ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) ) )
182 23 181 syl5eq 
 |-  ( ph -> ran ( x e. ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |-> ( x i^i X_ k e. A S ) ) = ( { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } u. ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) ) )
183 19 182 eqtrd 
 |-  ( ph -> ( ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |`t X_ k e. A S ) = ( { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } u. ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) ) )
184 183 fveq2d 
 |-  ( ph -> ( fi ` ( ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) |`t X_ k e. A S ) ) = ( fi ` ( { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } u. ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) ) ) )
185 4 184 eqtr3id 
 |-  ( ph -> ( ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) |`t X_ k e. A S ) = ( fi ` ( { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } u. ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) ) ) )
186 185 fveq2d 
 |-  ( ph -> ( topGen ` ( ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) |`t X_ k e. A S ) ) = ( topGen ` ( fi ` ( { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } u. ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) ) ) ) )
187 eqid 
 |-  U. ( Xt_ ` F ) = U. ( Xt_ ` F )
188 72 187 8 ptval2 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) = ( topGen ` ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) ) )
189 1 2 188 syl2anc 
 |-  ( ph -> ( Xt_ ` F ) = ( topGen ` ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) ) )
190 189 oveq1d 
 |-  ( ph -> ( ( Xt_ ` F ) |`t X_ k e. A S ) = ( ( topGen ` ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) ) |`t X_ k e. A S ) )
191 fvex 
 |-  ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) e. _V
192 tgrest 
 |-  ( ( ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) e. _V /\ X_ k e. A S e. _V ) -> ( topGen ` ( ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) |`t X_ k e. A S ) ) = ( ( topGen ` ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) ) |`t X_ k e. A S ) )
193 191 17 192 sylancr 
 |-  ( ph -> ( topGen ` ( ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) |`t X_ k e. A S ) ) = ( ( topGen ` ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) ) |`t X_ k e. A S ) )
194 190 193 eqtr4d 
 |-  ( ph -> ( ( Xt_ ` F ) |`t X_ k e. A S ) = ( topGen ` ( ( fi ` ( { U. ( Xt_ ` F ) } u. ran ( u e. A , v e. ( F ` u ) |-> ( `' ( w e. U. ( Xt_ ` F ) |-> ( w ` u ) ) " v ) ) ) ) |`t X_ k e. A S ) ) )
195 eqid 
 |-  U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) = U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) )
196 79 195 178 ptval2 
 |-  ( ( A e. V /\ ( k e. A |-> ( ( F ` k ) |`t S ) ) : A --> Top ) -> ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) = ( topGen ` ( fi ` ( { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } u. ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) ) ) ) )
197 1 78 196 syl2anc 
 |-  ( ph -> ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) = ( topGen ` ( fi ` ( { U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) } u. ran ( u e. A , v e. ( ( k e. A |-> ( ( F ` k ) |`t S ) ) ` u ) |-> ( `' ( w e. U. ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) |-> ( w ` u ) ) " v ) ) ) ) ) )
198 186 194 197 3eqtr4d 
 |-  ( ph -> ( ( Xt_ ` F ) |`t X_ k e. A S ) = ( Xt_ ` ( k e. A |-> ( ( F ` k ) |`t S ) ) ) )