Metamath Proof Explorer

Theorem xkococnlem

Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses xkococn.1 
|- F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) )
xkococn.s 
|- ( ph -> S e. N-Locally Comp )
xkococn.k 
|- ( ph -> K C_ U. R )
xkococn.c 
|- ( ph -> ( R |`t K ) e. Comp )
xkococn.v 
|- ( ph -> V e. T )
xkococn.a 
|- ( ph -> A e. ( S Cn T ) )
xkococn.b 
|- ( ph -> B e. ( R Cn S ) )
xkococn.i 
|- ( ph -> ( ( A o. B ) " K ) C_ V )
Assertion xkococnlem 
|- ( ph -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )

Proof

Step Hyp Ref Expression
1 xkococn.1 
 |-  F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) )
2 xkococn.s 
 |-  ( ph -> S e. N-Locally Comp )
3 xkococn.k 
 |-  ( ph -> K C_ U. R )
4 xkococn.c 
 |-  ( ph -> ( R |`t K ) e. Comp )
5 xkococn.v 
 |-  ( ph -> V e. T )
6 xkococn.a 
 |-  ( ph -> A e. ( S Cn T ) )
7 xkococn.b 
 |-  ( ph -> B e. ( R Cn S ) )
8 xkococn.i 
 |-  ( ph -> ( ( A o. B ) " K ) C_ V )
9 imacmp 
 |-  ( ( B e. ( R Cn S ) /\ ( R |`t K ) e. Comp ) -> ( S |`t ( B " K ) ) e. Comp )
10 7 4 9 syl2anc 
 |-  ( ph -> ( S |`t ( B " K ) ) e. Comp )
11 2 adantr 
 |-  ( ( ph /\ x e. ( B " K ) ) -> S e. N-Locally Comp )
12 cnima 
 |-  ( ( A e. ( S Cn T ) /\ V e. T ) -> ( `' A " V ) e. S )
13 6 5 12 syl2anc 
 |-  ( ph -> ( `' A " V ) e. S )
14 13 adantr 
 |-  ( ( ph /\ x e. ( B " K ) ) -> ( `' A " V ) e. S )
15 imaco 
 |-  ( ( A o. B ) " K ) = ( A " ( B " K ) )
16 15 8 eqsstrrid 
 |-  ( ph -> ( A " ( B " K ) ) C_ V )
17 eqid 
 |-  U. S = U. S
18 eqid 
 |-  U. T = U. T
19 17 18 cnf 
 |-  ( A e. ( S Cn T ) -> A : U. S --> U. T )
20 ffun 
 |-  ( A : U. S --> U. T -> Fun A )
21 6 19 20 3syl 
 |-  ( ph -> Fun A )
22 imassrn 
 |-  ( B " K ) C_ ran B
23 eqid 
 |-  U. R = U. R
24 23 17 cnf 
 |-  ( B e. ( R Cn S ) -> B : U. R --> U. S )
25 frn 
 |-  ( B : U. R --> U. S -> ran B C_ U. S )
26 7 24 25 3syl 
 |-  ( ph -> ran B C_ U. S )
27 22 26 sstrid 
 |-  ( ph -> ( B " K ) C_ U. S )
28 fdm 
 |-  ( A : U. S --> U. T -> dom A = U. S )
29 6 19 28 3syl 
 |-  ( ph -> dom A = U. S )
30 27 29 sseqtrrd 
 |-  ( ph -> ( B " K ) C_ dom A )
31 funimass3 
 |-  ( ( Fun A /\ ( B " K ) C_ dom A ) -> ( ( A " ( B " K ) ) C_ V <-> ( B " K ) C_ ( `' A " V ) ) )
32 21 30 31 syl2anc 
 |-  ( ph -> ( ( A " ( B " K ) ) C_ V <-> ( B " K ) C_ ( `' A " V ) ) )
33 16 32 mpbid 
 |-  ( ph -> ( B " K ) C_ ( `' A " V ) )
34 33 sselda 
 |-  ( ( ph /\ x e. ( B " K ) ) -> x e. ( `' A " V ) )
35 nlly2i 
 |-  ( ( S e. N-Locally Comp /\ ( `' A " V ) e. S /\ x e. ( `' A " V ) ) -> E. s e. ~P ( `' A " V ) E. u e. S ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) )
36 11 14 34 35 syl3anc 
 |-  ( ( ph /\ x e. ( B " K ) ) -> E. s e. ~P ( `' A " V ) E. u e. S ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) )
37 nllytop 
 |-  ( S e. N-Locally Comp -> S e. Top )
38 2 37 syl 
 |-  ( ph -> S e. Top )
39 38 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> S e. Top )
40 imaexg 
 |-  ( B e. ( R Cn S ) -> ( B " K ) e. _V )
41 7 40 syl 
 |-  ( ph -> ( B " K ) e. _V )
42 41 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> ( B " K ) e. _V )
43 simprl 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> u e. S )
44 elrestr 
 |-  ( ( S e. Top /\ ( B " K ) e. _V /\ u e. S ) -> ( u i^i ( B " K ) ) e. ( S |`t ( B " K ) ) )
45 39 42 43 44 syl3anc 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> ( u i^i ( B " K ) ) e. ( S |`t ( B " K ) ) )
46 simprr1 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> x e. u )
47 simpllr 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> x e. ( B " K ) )
48 46 47 elind 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> x e. ( u i^i ( B " K ) ) )
49 inss1 
 |-  ( u i^i ( B " K ) ) C_ u
50 elpwi 
 |-  ( s e. ~P ( `' A " V ) -> s C_ ( `' A " V ) )
51 50 ad2antlr 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> s C_ ( `' A " V ) )
52 elssuni 
 |-  ( ( `' A " V ) e. S -> ( `' A " V ) C_ U. S )
53 13 52 syl 
 |-  ( ph -> ( `' A " V ) C_ U. S )
54 53 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> ( `' A " V ) C_ U. S )
55 51 54 sstrd 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> s C_ U. S )
56 simprr2 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> u C_ s )
57 17 ssntr 
 |-  ( ( ( S e. Top /\ s C_ U. S ) /\ ( u e. S /\ u C_ s ) ) -> u C_ ( ( int ` S ) ` s ) )
58 39 55 43 56 57 syl22anc 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> u C_ ( ( int ` S ) ` s ) )
59 49 58 sstrid 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) )
60 simprr3 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> ( S |`t s ) e. Comp )
61 59 60 jca 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> ( ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) )
62 eleq2 
 |-  ( y = ( u i^i ( B " K ) ) -> ( x e. y <-> x e. ( u i^i ( B " K ) ) ) )
63 cleq1lem 
 |-  ( y = ( u i^i ( B " K ) ) -> ( ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) <-> ( ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
64 62 63 anbi12d 
 |-  ( y = ( u i^i ( B " K ) ) -> ( ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) <-> ( x e. ( u i^i ( B " K ) ) /\ ( ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) ) )
65 64 rspcev 
 |-  ( ( ( u i^i ( B " K ) ) e. ( S |`t ( B " K ) ) /\ ( x e. ( u i^i ( B " K ) ) /\ ( ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) ) -> E. y e. ( S |`t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
66 45 48 61 65 syl12anc 
 |-  ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) ) ) -> E. y e. ( S |`t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
67 66 rexlimdvaa 
 |-  ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) -> ( E. u e. S ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) -> E. y e. ( S |`t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) ) )
68 67 reximdva 
 |-  ( ( ph /\ x e. ( B " K ) ) -> ( E. s e. ~P ( `' A " V ) E. u e. S ( x e. u /\ u C_ s /\ ( S |`t s ) e. Comp ) -> E. s e. ~P ( `' A " V ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) ) )
69 36 68 mpd 
 |-  ( ( ph /\ x e. ( B " K ) ) -> E. s e. ~P ( `' A " V ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
70 rexcom 
 |-  ( E. s e. ~P ( `' A " V ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) <-> E. y e. ( S |`t ( B " K ) ) E. s e. ~P ( `' A " V ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
71 r19.42v 
 |-  ( E. s e. ~P ( `' A " V ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) <-> ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
72 71 rexbii 
 |-  ( E. y e. ( S |`t ( B " K ) ) E. s e. ~P ( `' A " V ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) <-> E. y e. ( S |`t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
73 70 72 bitri 
 |-  ( E. s e. ~P ( `' A " V ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) <-> E. y e. ( S |`t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
74 69 73 sylib 
 |-  ( ( ph /\ x e. ( B " K ) ) -> E. y e. ( S |`t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
75 74 ralrimiva 
 |-  ( ph -> A. x e. ( B " K ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
76 17 restuni 
 |-  ( ( S e. Top /\ ( B " K ) C_ U. S ) -> ( B " K ) = U. ( S |`t ( B " K ) ) )
77 38 27 76 syl2anc 
 |-  ( ph -> ( B " K ) = U. ( S |`t ( B " K ) ) )
78 77 raleqdv 
 |-  ( ph -> ( A. x e. ( B " K ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) <-> A. x e. U. ( S |`t ( B " K ) ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) ) )
79 75 78 mpbid 
 |-  ( ph -> A. x e. U. ( S |`t ( B " K ) ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) )
80 eqid 
 |-  U. ( S |`t ( B " K ) ) = U. ( S |`t ( B " K ) )
81 fveq2 
 |-  ( s = ( k ` y ) -> ( ( int ` S ) ` s ) = ( ( int ` S ) ` ( k ` y ) ) )
82 81 sseq2d 
 |-  ( s = ( k ` y ) -> ( y C_ ( ( int ` S ) ` s ) <-> y C_ ( ( int ` S ) ` ( k ` y ) ) ) )
83 oveq2 
 |-  ( s = ( k ` y ) -> ( S |`t s ) = ( S |`t ( k ` y ) ) )
84 83 eleq1d 
 |-  ( s = ( k ` y ) -> ( ( S |`t s ) e. Comp <-> ( S |`t ( k ` y ) ) e. Comp ) )
85 82 84 anbi12d 
 |-  ( s = ( k ` y ) -> ( ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) <-> ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) )
86 80 85 cmpcovf 
 |-  ( ( ( S |`t ( B " K ) ) e. Comp /\ A. x e. U. ( S |`t ( B " K ) ) E. y e. ( S |`t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S |`t s ) e. Comp ) ) ) -> E. w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ( U. ( S |`t ( B " K ) ) = U. w /\ E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) )
87 10 79 86 syl2anc 
 |-  ( ph -> E. w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ( U. ( S |`t ( B " K ) ) = U. w /\ E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) )
88 77 adantr 
 |-  ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) -> ( B " K ) = U. ( S |`t ( B " K ) ) )
89 88 eqeq1d 
 |-  ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) -> ( ( B " K ) = U. w <-> U. ( S |`t ( B " K ) ) = U. w ) )
90 89 biimpar 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ U. ( S |`t ( B " K ) ) = U. w ) -> ( B " K ) = U. w )
91 38 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> S e. Top )
92 cntop2 
 |-  ( A e. ( S Cn T ) -> T e. Top )
93 6 92 syl 
 |-  ( ph -> T e. Top )
94 93 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> T e. Top )
95 xkotop 
 |-  ( ( S e. Top /\ T e. Top ) -> ( T ^ko S ) e. Top )
96 91 94 95 syl2anc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( T ^ko S ) e. Top )
97 cntop1 
 |-  ( B e. ( R Cn S ) -> R e. Top )
98 7 97 syl 
 |-  ( ph -> R e. Top )
99 98 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> R e. Top )
100 xkotop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top )
101 99 91 100 syl2anc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( S ^ko R ) e. Top )
102 simprrl 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> k : w --> ~P ( `' A " V ) )
103 102 frnd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ran k C_ ~P ( `' A " V ) )
104 sspwuni 
 |-  ( ran k C_ ~P ( `' A " V ) <-> U. ran k C_ ( `' A " V ) )
105 103 104 sylib 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U. ran k C_ ( `' A " V ) )
106 13 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( `' A " V ) e. S )
107 106 52 syl 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( `' A " V ) C_ U. S )
108 105 107 sstrd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U. ran k C_ U. S )
109 ffn 
 |-  ( k : w --> ~P ( `' A " V ) -> k Fn w )
110 fniunfv 
 |-  ( k Fn w -> U_ y e. w ( k ` y ) = U. ran k )
111 102 109 110 3syl 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( k ` y ) = U. ran k )
112 111 oveq2d 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( S |`t U_ y e. w ( k ` y ) ) = ( S |`t U. ran k ) )
113 simplr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) )
114 113 elin2d 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> w e. Fin )
115 simprrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) )
116 simpr 
 |-  ( ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) -> ( S |`t ( k ` y ) ) e. Comp )
117 116 ralimi 
 |-  ( A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) -> A. y e. w ( S |`t ( k ` y ) ) e. Comp )
118 115 117 syl 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( S |`t ( k ` y ) ) e. Comp )
119 17 fiuncmp 
 |-  ( ( S e. Top /\ w e. Fin /\ A. y e. w ( S |`t ( k ` y ) ) e. Comp ) -> ( S |`t U_ y e. w ( k ` y ) ) e. Comp )
120 91 114 118 119 syl3anc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( S |`t U_ y e. w ( k ` y ) ) e. Comp )
121 112 120 eqeltrrd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( S |`t U. ran k ) e. Comp )
122 5 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> V e. T )
123 17 91 94 108 121 122 xkoopn 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } e. ( T ^ko S ) )
124 3 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> K C_ U. R )
125 4 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( R |`t K ) e. Comp )
126 111 108 eqsstrd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( k ` y ) C_ U. S )
127 iunss 
 |-  ( U_ y e. w ( k ` y ) C_ U. S <-> A. y e. w ( k ` y ) C_ U. S )
128 126 127 sylib 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( k ` y ) C_ U. S )
129 17 ntropn 
 |-  ( ( S e. Top /\ ( k ` y ) C_ U. S ) -> ( ( int ` S ) ` ( k ` y ) ) e. S )
130 129 ex 
 |-  ( S e. Top -> ( ( k ` y ) C_ U. S -> ( ( int ` S ) ` ( k ` y ) ) e. S ) )
131 130 ralimdv 
 |-  ( S e. Top -> ( A. y e. w ( k ` y ) C_ U. S -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) e. S ) )
132 91 128 131 sylc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) e. S )
133 iunopn 
 |-  ( ( S e. Top /\ A. y e. w ( ( int ` S ) ` ( k ` y ) ) e. S ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) e. S )
134 91 132 133 syl2anc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) e. S )
135 23 99 91 124 125 134 xkoopn 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } e. ( S ^ko R ) )
136 txopn 
 |-  ( ( ( ( T ^ko S ) e. Top /\ ( S ^ko R ) e. Top ) /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } e. ( T ^ko S ) /\ { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } e. ( S ^ko R ) ) ) -> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) )
137 96 101 123 135 136 syl22anc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) )
138 imaeq1 
 |-  ( a = A -> ( a " U. ran k ) = ( A " U. ran k ) )
139 138 sseq1d 
 |-  ( a = A -> ( ( a " U. ran k ) C_ V <-> ( A " U. ran k ) C_ V ) )
140 6 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> A e. ( S Cn T ) )
141 imaiun 
 |-  ( A " U_ y e. w ( k ` y ) ) = U_ y e. w ( A " ( k ` y ) )
142 111 imaeq2d 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( A " U_ y e. w ( k ` y ) ) = ( A " U. ran k ) )
143 141 142 eqtr3id 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( A " ( k ` y ) ) = ( A " U. ran k ) )
144 111 105 eqsstrd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( k ` y ) C_ ( `' A " V ) )
145 21 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> Fun A )
146 102 109 syl 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> k Fn w )
147 29 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> dom A = U. S )
148 108 147 sseqtrrd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U. ran k C_ dom A )
149 simpl1 
 |-  ( ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) /\ y e. w ) -> Fun A )
150 110 3ad2ant2 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U_ y e. w ( k ` y ) = U. ran k )
151 simp3 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U. ran k C_ dom A )
152 150 151 eqsstrd 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U_ y e. w ( k ` y ) C_ dom A )
153 iunss 
 |-  ( U_ y e. w ( k ` y ) C_ dom A <-> A. y e. w ( k ` y ) C_ dom A )
154 152 153 sylib 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> A. y e. w ( k ` y ) C_ dom A )
155 154 r19.21bi 
 |-  ( ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) /\ y e. w ) -> ( k ` y ) C_ dom A )
156 funimass3 
 |-  ( ( Fun A /\ ( k ` y ) C_ dom A ) -> ( ( A " ( k ` y ) ) C_ V <-> ( k ` y ) C_ ( `' A " V ) ) )
157 149 155 156 syl2anc 
 |-  ( ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) /\ y e. w ) -> ( ( A " ( k ` y ) ) C_ V <-> ( k ` y ) C_ ( `' A " V ) ) )
158 157 ralbidva 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> ( A. y e. w ( A " ( k ` y ) ) C_ V <-> A. y e. w ( k ` y ) C_ ( `' A " V ) ) )
159 iunss 
 |-  ( U_ y e. w ( A " ( k ` y ) ) C_ V <-> A. y e. w ( A " ( k ` y ) ) C_ V )
160 iunss 
 |-  ( U_ y e. w ( k ` y ) C_ ( `' A " V ) <-> A. y e. w ( k ` y ) C_ ( `' A " V ) )
161 158 159 160 3bitr4g 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> ( U_ y e. w ( A " ( k ` y ) ) C_ V <-> U_ y e. w ( k ` y ) C_ ( `' A " V ) ) )
162 145 146 148 161 syl3anc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( U_ y e. w ( A " ( k ` y ) ) C_ V <-> U_ y e. w ( k ` y ) C_ ( `' A " V ) ) )
163 144 162 mpbird 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( A " ( k ` y ) ) C_ V )
164 143 163 eqsstrrd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( A " U. ran k ) C_ V )
165 139 140 164 elrabd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> A e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } )
166 imaeq1 
 |-  ( b = B -> ( b " K ) = ( B " K ) )
167 166 sseq1d 
 |-  ( b = B -> ( ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) <-> ( B " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) )
168 7 ad2antrr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> B e. ( R Cn S ) )
169 simprl 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( B " K ) = U. w )
170 uniiun 
 |-  U. w = U_ y e. w y
171 169 170 eqtrdi 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( B " K ) = U_ y e. w y )
172 simpl 
 |-  ( ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) -> y C_ ( ( int ` S ) ` ( k ` y ) ) )
173 172 ralimi 
 |-  ( A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) -> A. y e. w y C_ ( ( int ` S ) ` ( k ` y ) ) )
174 ss2iun 
 |-  ( A. y e. w y C_ ( ( int ` S ) ` ( k ` y ) ) -> U_ y e. w y C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) )
175 115 173 174 3syl 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w y C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) )
176 171 175 eqsstrd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( B " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) )
177 167 168 176 elrabd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> B e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } )
178 165 177 opelxpd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) )
179 imaeq1 
 |-  ( a = u -> ( a " U. ran k ) = ( u " U. ran k ) )
180 179 sseq1d 
 |-  ( a = u -> ( ( a " U. ran k ) C_ V <-> ( u " U. ran k ) C_ V ) )
181 180 elrab 
 |-  ( u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } <-> ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) )
182 imaeq1 
 |-  ( b = v -> ( b " K ) = ( v " K ) )
183 182 sseq1d 
 |-  ( b = v -> ( ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) <-> ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) )
184 183 elrab 
 |-  ( v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } <-> ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) )
185 181 184 anbi12i 
 |-  ( ( u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } /\ v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) <-> ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) )
186 simprll 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> u e. ( S Cn T ) )
187 simprrl 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> v e. ( R Cn S ) )
188 coeq1 
 |-  ( f = u -> ( f o. g ) = ( u o. g ) )
189 coeq2 
 |-  ( g = v -> ( u o. g ) = ( u o. v ) )
190 vex 
 |-  u e. _V
191 vex 
 |-  v e. _V
192 190 191 coex 
 |-  ( u o. v ) e. _V
193 188 189 1 192 ovmpo 
 |-  ( ( u e. ( S Cn T ) /\ v e. ( R Cn S ) ) -> ( u F v ) = ( u o. v ) )
194 186 187 193 syl2anc 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u F v ) = ( u o. v ) )
195 imaeq1 
 |-  ( h = ( u o. v ) -> ( h " K ) = ( ( u o. v ) " K ) )
196 195 sseq1d 
 |-  ( h = ( u o. v ) -> ( ( h " K ) C_ V <-> ( ( u o. v ) " K ) C_ V ) )
197 cnco 
 |-  ( ( v e. ( R Cn S ) /\ u e. ( S Cn T ) ) -> ( u o. v ) e. ( R Cn T ) )
198 187 186 197 syl2anc 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u o. v ) e. ( R Cn T ) )
199 imaco 
 |-  ( ( u o. v ) " K ) = ( u " ( v " K ) )
200 simprrr 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) )
201 17 ntrss2 
 |-  ( ( S e. Top /\ ( k ` y ) C_ U. S ) -> ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) )
202 201 ex 
 |-  ( S e. Top -> ( ( k ` y ) C_ U. S -> ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) ) )
203 202 ralimdv 
 |-  ( S e. Top -> ( A. y e. w ( k ` y ) C_ U. S -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) ) )
204 91 128 203 sylc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) )
205 ss2iun 
 |-  ( A. y e. w ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) C_ U_ y e. w ( k ` y ) )
206 204 205 syl 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) C_ U_ y e. w ( k ` y ) )
207 206 111 sseqtrd 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) C_ U. ran k )
208 207 adantr 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) C_ U. ran k )
209 200 208 sstrd 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( v " K ) C_ U. ran k )
210 imass2 
 |-  ( ( v " K ) C_ U. ran k -> ( u " ( v " K ) ) C_ ( u " U. ran k ) )
211 209 210 syl 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u " ( v " K ) ) C_ ( u " U. ran k ) )
212 simprlr 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u " U. ran k ) C_ V )
213 211 212 sstrd 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u " ( v " K ) ) C_ V )
214 199 213 eqsstrid 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( ( u o. v ) " K ) C_ V )
215 196 198 214 elrabd 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u o. v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
216 194 215 eqeltrd 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
217 185 216 sylan2b 
 |-  ( ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) /\ ( u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } /\ v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) -> ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
218 217 ralrimivva 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> A. u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } A. v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
219 1 mpofun 
 |-  Fun F
220 ssrab2 
 |-  { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } C_ ( S Cn T )
221 ssrab2 
 |-  { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } C_ ( R Cn S )
222 xpss12 
 |-  ( ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } C_ ( S Cn T ) /\ { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } C_ ( R Cn S ) ) -> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( ( S Cn T ) X. ( R Cn S ) ) )
223 220 221 222 mp2an 
 |-  ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( ( S Cn T ) X. ( R Cn S ) )
224 vex 
 |-  f e. _V
225 vex 
 |-  g e. _V
226 224 225 coex 
 |-  ( f o. g ) e. _V
227 1 226 dmmpo 
 |-  dom F = ( ( S Cn T ) X. ( R Cn S ) )
228 223 227 sseqtrri 
 |-  ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ dom F
229 funimassov 
 |-  ( ( Fun F /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ dom F ) -> ( ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } <-> A. u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } A. v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } ) )
230 219 228 229 mp2an 
 |-  ( ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } <-> A. u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } A. v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
231 218 230 sylibr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } )
232 funimass3 
 |-  ( ( Fun F /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ dom F ) -> ( ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } <-> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
233 219 228 232 mp2an 
 |-  ( ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } <-> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) )
234 231 233 sylib 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) )
235 eleq2 
 |-  ( z = ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) -> ( <. A , B >. e. z <-> <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) )
236 sseq1 
 |-  ( z = ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) -> ( z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) <-> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
237 235 236 anbi12d 
 |-  ( z = ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) -> ( ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) <-> ( <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
238 237 rspcev 
 |-  ( ( ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) /\ ( <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
239 137 178 234 238 syl12anc 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
240 239 expr 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( B " K ) = U. w ) -> ( ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
241 240 exlimdv 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ ( B " K ) = U. w ) -> ( E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
242 90 241 syldan 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ U. ( S |`t ( B " K ) ) = U. w ) -> ( E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
243 242 expimpd 
 |-  ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) -> ( ( U. ( S |`t ( B " K ) ) = U. w /\ E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
244 243 rexlimdva 
 |-  ( ph -> ( E. w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ( U. ( S |`t ( B " K ) ) = U. w /\ E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
245 87 244 mpd 
 |-  ( ph -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )