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 75 77 raleqtrdv 
 |-  ( 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 ) ) )
79 eqid 
 |-  U. ( S |`t ( B " K ) ) = U. ( S |`t ( B " K ) )
80 fveq2 
 |-  ( s = ( k ` y ) -> ( ( int ` S ) ` s ) = ( ( int ` S ) ` ( k ` y ) ) )
81 80 sseq2d 
 |-  ( s = ( k ` y ) -> ( y C_ ( ( int ` S ) ` s ) <-> y C_ ( ( int ` S ) ` ( k ` y ) ) ) )
82 oveq2 
 |-  ( s = ( k ` y ) -> ( S |`t s ) = ( S |`t ( k ` y ) ) )
83 82 eleq1d 
 |-  ( s = ( k ` y ) -> ( ( S |`t s ) e. Comp <-> ( S |`t ( k ` y ) ) e. Comp ) )
84 81 83 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 ) ) )
85 79 84 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 ) ) ) )
86 10 78 85 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 ) ) ) )
87 77 adantr 
 |-  ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) -> ( B " K ) = U. ( S |`t ( B " K ) ) )
88 87 eqeq1d 
 |-  ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) -> ( ( B " K ) = U. w <-> U. ( S |`t ( B " K ) ) = U. w ) )
89 88 biimpar 
 |-  ( ( ( ph /\ w e. ( ~P ( S |`t ( B " K ) ) i^i Fin ) ) /\ U. ( S |`t ( B " K ) ) = U. w ) -> ( B " K ) = U. w )
90 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 )
91 cntop2 
 |-  ( A e. ( S Cn T ) -> T e. Top )
92 6 91 syl 
 |-  ( ph -> T e. Top )
93 92 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 )
94 xkotop 
 |-  ( ( S e. Top /\ T e. Top ) -> ( T ^ko S ) e. Top )
95 90 93 94 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 )
96 cntop1 
 |-  ( B e. ( R Cn S ) -> R e. Top )
97 7 96 syl 
 |-  ( ph -> R e. Top )
98 97 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 )
99 xkotop 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top )
100 98 90 99 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 )
101 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 ) )
102 101 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 ) )
103 sspwuni 
 |-  ( ran k C_ ~P ( `' A " V ) <-> U. ran k C_ ( `' A " V ) )
104 102 103 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 ) )
105 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 )
106 105 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 )
107 104 106 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 )
108 ffn 
 |-  ( k : w --> ~P ( `' A " V ) -> k Fn w )
109 fniunfv 
 |-  ( k Fn w -> U_ y e. w ( k ` y ) = U. ran k )
110 101 108 109 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 )
111 110 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 ) )
112 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 ) )
113 112 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 )
114 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 ) )
115 simpr 
 |-  ( ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) -> ( S |`t ( k ` y ) ) e. Comp )
116 115 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 )
117 114 116 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 )
118 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 )
119 90 113 117 118 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 )
120 111 119 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 )
121 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 )
122 17 90 93 107 120 121 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 ) )
123 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 )
124 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 )
125 110 107 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 )
126 iunss 
 |-  ( U_ y e. w ( k ` y ) C_ U. S <-> A. y e. w ( k ` y ) C_ U. S )
127 125 126 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 )
128 17 ntropn 
 |-  ( ( S e. Top /\ ( k ` y ) C_ U. S ) -> ( ( int ` S ) ` ( k ` y ) ) e. S )
129 128 ex 
 |-  ( S e. Top -> ( ( k ` y ) C_ U. S -> ( ( int ` S ) ` ( k ` y ) ) e. S ) )
130 129 ralimdv 
 |-  ( S e. Top -> ( A. y e. w ( k ` y ) C_ U. S -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) e. S ) )
131 90 127 130 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 )
132 iunopn 
 |-  ( ( S e. Top /\ A. y e. w ( ( int ` S ) ` ( k ` y ) ) e. S ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) e. S )
133 90 131 132 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 )
134 23 98 90 123 124 133 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 ) )
135 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 ) ) )
136 95 100 122 134 135 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 ) ) )
137 imaeq1 
 |-  ( a = A -> ( a " U. ran k ) = ( A " U. ran k ) )
138 137 sseq1d 
 |-  ( a = A -> ( ( a " U. ran k ) C_ V <-> ( A " U. ran k ) C_ V ) )
139 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 ) )
140 imaiun 
 |-  ( A " U_ y e. w ( k ` y ) ) = U_ y e. w ( A " ( k ` y ) )
141 110 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 ) )
142 140 141 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 ) )
143 110 104 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 ) )
144 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 )
145 101 108 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 )
146 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 )
147 107 146 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 )
148 simpl1 
 |-  ( ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) /\ y e. w ) -> Fun A )
149 109 3ad2ant2 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U_ y e. w ( k ` y ) = U. ran k )
150 simp3 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U. ran k C_ dom A )
151 149 150 eqsstrd 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U_ y e. w ( k ` y ) C_ dom A )
152 iunss 
 |-  ( U_ y e. w ( k ` y ) C_ dom A <-> A. y e. w ( k ` y ) C_ dom A )
153 151 152 sylib 
 |-  ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> A. y e. w ( k ` y ) C_ dom A )
154 153 r19.21bi 
 |-  ( ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) /\ y e. w ) -> ( k ` y ) C_ dom A )
155 funimass3 
 |-  ( ( Fun A /\ ( k ` y ) C_ dom A ) -> ( ( A " ( k ` y ) ) C_ V <-> ( k ` y ) C_ ( `' A " V ) ) )
156 148 154 155 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 ) ) )
157 156 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 ) ) )
158 iunss 
 |-  ( U_ y e. w ( A " ( k ` y ) ) C_ V <-> A. y e. w ( A " ( k ` y ) ) C_ V )
159 iunss 
 |-  ( U_ y e. w ( k ` y ) C_ ( `' A " V ) <-> A. y e. w ( k ` y ) C_ ( `' A " V ) )
160 157 158 159 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 ) ) )
161 144 145 147 160 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 ) ) )
162 143 161 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 )
163 142 162 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 )
164 138 139 163 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 } )
165 imaeq1 
 |-  ( b = B -> ( b " K ) = ( B " K ) )
166 165 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 ) ) ) )
167 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 ) )
168 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 )
169 uniiun 
 |-  U. w = U_ y e. w y
170 168 169 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 )
171 simpl 
 |-  ( ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S |`t ( k ` y ) ) e. Comp ) -> y C_ ( ( int ` S ) ` ( k ` y ) ) )
172 171 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 ) ) )
173 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 ) ) )
174 114 172 173 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 ) ) )
175 170 174 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 ) ) )
176 166 167 175 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 ) ) } )
177 164 176 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 ) ) } ) )
178 imaeq1 
 |-  ( a = u -> ( a " U. ran k ) = ( u " U. ran k ) )
179 178 sseq1d 
 |-  ( a = u -> ( ( a " U. ran k ) C_ V <-> ( u " U. ran k ) C_ V ) )
180 179 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 ) )
181 imaeq1 
 |-  ( b = v -> ( b " K ) = ( v " K ) )
182 181 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 ) ) ) )
183 182 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 ) ) ) )
184 180 183 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 ) ) ) ) )
185 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 ) )
186 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 ) )
187 coeq1 
 |-  ( f = u -> ( f o. g ) = ( u o. g ) )
188 coeq2 
 |-  ( g = v -> ( u o. g ) = ( u o. v ) )
189 vex 
 |-  u e. _V
190 vex 
 |-  v e. _V
191 189 190 coex 
 |-  ( u o. v ) e. _V
192 187 188 1 191 ovmpo 
 |-  ( ( u e. ( S Cn T ) /\ v e. ( R Cn S ) ) -> ( u F v ) = ( u o. v ) )
193 185 186 192 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 ) )
194 imaeq1 
 |-  ( h = ( u o. v ) -> ( h " K ) = ( ( u o. v ) " K ) )
195 194 sseq1d 
 |-  ( h = ( u o. v ) -> ( ( h " K ) C_ V <-> ( ( u o. v ) " K ) C_ V ) )
196 cnco 
 |-  ( ( v e. ( R Cn S ) /\ u e. ( S Cn T ) ) -> ( u o. v ) e. ( R Cn T ) )
197 186 185 196 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 ) )
198 imaco 
 |-  ( ( u o. v ) " K ) = ( u " ( v " K ) )
199 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 ) ) )
200 17 ntrss2 
 |-  ( ( S e. Top /\ ( k ` y ) C_ U. S ) -> ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) )
201 200 ex 
 |-  ( S e. Top -> ( ( k ` y ) C_ U. S -> ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) ) )
202 201 ralimdv 
 |-  ( S e. Top -> ( A. y e. w ( k ` y ) C_ U. S -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) ) )
203 90 127 202 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 ) )
204 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 ) )
205 203 204 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 ) )
206 205 110 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 )
207 206 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 )
208 199 207 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 )
209 imass2 
 |-  ( ( v " K ) C_ U. ran k -> ( u " ( v " K ) ) C_ ( u " U. ran k ) )
210 208 209 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 ) )
211 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 )
212 210 211 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 )
213 198 212 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 )
214 195 197 213 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 } )
215 193 214 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 } )
216 184 215 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 } )
217 216 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 } )
218 1 mpofun 
 |-  Fun F
219 ssrab2 
 |-  { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } C_ ( S Cn T )
220 ssrab2 
 |-  { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } C_ ( R Cn S )
221 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 ) ) )
222 219 220 221 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 ) )
223 vex 
 |-  f e. _V
224 vex 
 |-  g e. _V
225 223 224 coex 
 |-  ( f o. g ) e. _V
226 1 225 dmmpo 
 |-  dom F = ( ( S Cn T ) X. ( R Cn S ) )
227 222 226 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
228 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 } ) )
229 218 227 228 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 } )
230 217 229 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 } )
231 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 } ) ) )
232 218 227 231 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 } ) )
233 230 232 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 } ) )
234 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 ) ) } ) ) )
235 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 } ) ) )
236 234 235 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 } ) ) ) )
237 236 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 } ) ) )
238 136 177 233 237 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 } ) ) )
239 238 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 } ) ) ) )
240 239 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 } ) ) ) )
241 89 240 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 } ) ) ) )
242 241 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 } ) ) ) )
243 242 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 } ) ) ) )
244 86 243 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 } ) ) )