MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkococnlem Structured version   Unicode version

Theorem xkococnlem 19232
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.)
Hypotheses
Ref Expression
xkococn.1  |-  F  =  ( f  e.  ( S  Cn  T ) ,  g  e.  ( R  Cn  S ) 
|->  ( f  o.  g
) )
xkococn.s  |-  ( ph  ->  S  e. 𝑛Locally  Comp )
xkococn.k  |-  ( ph  ->  K  C_  U. R )
xkococn.c  |-  ( ph  ->  ( Rt  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
Ref Expression
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 } ) ) )
Distinct variable groups:    z, A    z, B    f, g, h, z, R    S, f,
g, z    h, K, z    T, f, g, h, z    z, F    h, V, z
Allowed substitution hints:    ph( z, f, g, h)    A( f,
g, h)    B( f,
g, h)    S( h)    F( f, g, h)    K( f, g)    V( f, g)

Proof of Theorem xkococnlem
Dummy variables  k 
a  s  u  v  w  x  y  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkococn.b . . . 4  |-  ( ph  ->  B  e.  ( R  Cn  S ) )
2 xkococn.c . . . 4  |-  ( ph  ->  ( Rt  K )  e.  Comp )
3 imacmp 19000 . . . 4  |-  ( ( B  e.  ( R  Cn  S )  /\  ( Rt  K )  e.  Comp )  ->  ( St  ( B
" K ) )  e.  Comp )
41, 2, 3syl2anc 661 . . 3  |-  ( ph  ->  ( St  ( B " K ) )  e. 
Comp )
5 xkococn.s . . . . . . . . 9  |-  ( ph  ->  S  e. 𝑛Locally  Comp )
65adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  S  e. 𝑛Locally  Comp )
7 xkococn.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  ( S  Cn  T ) )
8 xkococn.v . . . . . . . . . 10  |-  ( ph  ->  V  e.  T )
9 cnima 18869 . . . . . . . . . 10  |-  ( ( A  e.  ( S  Cn  T )  /\  V  e.  T )  ->  ( `' A " V )  e.  S
)
107, 8, 9syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( `' A " V )  e.  S
)
1110adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  ( `' A " V )  e.  S )
12 imaco 5343 . . . . . . . . . . 11  |-  ( ( A  o.  B )
" K )  =  ( A " ( B " K ) )
13 xkococn.i . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  o.  B ) " K
)  C_  V )
1412, 13syl5eqssr 3401 . . . . . . . . . 10  |-  ( ph  ->  ( A " ( B " K ) ) 
C_  V )
15 eqid 2443 . . . . . . . . . . . . 13  |-  U. S  =  U. S
16 eqid 2443 . . . . . . . . . . . . 13  |-  U. T  =  U. T
1715, 16cnf 18850 . . . . . . . . . . . 12  |-  ( A  e.  ( S  Cn  T )  ->  A : U. S --> U. T
)
18 ffun 5561 . . . . . . . . . . . 12  |-  ( A : U. S --> U. T  ->  Fun  A )
197, 17, 183syl 20 . . . . . . . . . . 11  |-  ( ph  ->  Fun  A )
20 imassrn 5180 . . . . . . . . . . . . 13  |-  ( B
" K )  C_  ran  B
21 eqid 2443 . . . . . . . . . . . . . . 15  |-  U. R  =  U. R
2221, 15cnf 18850 . . . . . . . . . . . . . 14  |-  ( B  e.  ( R  Cn  S )  ->  B : U. R --> U. S
)
23 frn 5565 . . . . . . . . . . . . . 14  |-  ( B : U. R --> U. S  ->  ran  B  C_  U. S
)
241, 22, 233syl 20 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  B  C_  U. S
)
2520, 24syl5ss 3367 . . . . . . . . . . . 12  |-  ( ph  ->  ( B " K
)  C_  U. S )
26 fdm 5563 . . . . . . . . . . . . 13  |-  ( A : U. S --> U. T  ->  dom  A  =  U. S )
277, 17, 263syl 20 . . . . . . . . . . . 12  |-  ( ph  ->  dom  A  =  U. S )
2825, 27sseqtr4d 3393 . . . . . . . . . . 11  |-  ( ph  ->  ( B " K
)  C_  dom  A )
29 funimass3 5819 . . . . . . . . . . 11  |-  ( ( Fun  A  /\  ( B " K )  C_  dom  A )  ->  (
( A " ( B " K ) ) 
C_  V  <->  ( B " K )  C_  ( `' A " V ) ) )
3019, 28, 29syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( A "
( B " K
) )  C_  V  <->  ( B " K ) 
C_  ( `' A " V ) ) )
3114, 30mpbid 210 . . . . . . . . 9  |-  ( ph  ->  ( B " K
)  C_  ( `' A " V ) )
3231sselda 3356 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  x  e.  ( `' A " V ) )
33 nlly2i 19080 . . . . . . . 8  |-  ( ( S  e. 𝑛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  /\  ( St  s )  e. 
Comp ) )
346, 11, 32, 33syl3anc 1218 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  E. s  e.  ~P  ( `' A " V ) E. u  e.  S  ( x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp )
)
35 nllytop 19077 . . . . . . . . . . . . 13  |-  ( S  e. 𝑛Locally 
Comp  ->  S  e.  Top )
365, 35syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  Top )
3736ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  ->  S  e.  Top )
38 imaexg 6515 . . . . . . . . . . . . 13  |-  ( B  e.  ( R  Cn  S )  ->  ( B " K )  e. 
_V )
391, 38syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( B " K
)  e.  _V )
4039ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  -> 
( B " K
)  e.  _V )
41 simprl 755 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  ->  u  e.  S )
42 elrestr 14367 . . . . . . . . . . 11  |-  ( ( S  e.  Top  /\  ( B " K )  e.  _V  /\  u  e.  S )  ->  (
u  i^i  ( B " K ) )  e.  ( St  ( B " K ) ) )
4337, 40, 41, 42syl3anc 1218 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  -> 
( u  i^i  ( B " K ) )  e.  ( St  ( B
" K ) ) )
44 simprr1 1036 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  ->  x  e.  u )
45 simpllr 758 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  ->  x  e.  ( B " K ) )
4644, 45elind 3540 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  ->  x  e.  ( u  i^i  ( B " K
) ) )
47 inss1 3570 . . . . . . . . . . . 12  |-  ( u  i^i  ( B " K ) )  C_  u
48 elpwi 3869 . . . . . . . . . . . . . . 15  |-  ( s  e.  ~P ( `' A " V )  ->  s  C_  ( `' A " V ) )
4948ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  -> 
s  C_  ( `' A " V ) )
50 elssuni 4121 . . . . . . . . . . . . . . . 16  |-  ( ( `' A " V )  e.  S  ->  ( `' A " V ) 
C_  U. S )
5110, 50syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( `' A " V )  C_  U. S
)
5251ad3antrrr 729 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  -> 
( `' A " V )  C_  U. S
)
5349, 52sstrd 3366 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  -> 
s  C_  U. S )
54 simprr2 1037 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  ->  u  C_  s )
5515ssntr 18662 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  Top  /\  s  C_  U. S )  /\  ( u  e.  S  /\  u  C_  s ) )  ->  u  C_  ( ( int `  S ) `  s
) )
5637, 53, 41, 54, 55syl22anc 1219 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  ->  u  C_  ( ( int `  S ) `  s
) )
5747, 56syl5ss 3367 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  -> 
( u  i^i  ( B " K ) ) 
C_  ( ( int `  S ) `  s
) )
58 simprr3 1038 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  -> 
( St  s )  e. 
Comp )
5957, 58jca 532 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  -> 
( ( u  i^i  ( B " K
) )  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) )
60 eleq2 2504 . . . . . . . . . . . 12  |-  ( y  =  ( u  i^i  ( B " K
) )  ->  (
x  e.  y  <->  x  e.  ( u  i^i  ( B " K ) ) ) )
61 sseq1 3377 . . . . . . . . . . . . 13  |-  ( y  =  ( u  i^i  ( B " K
) )  ->  (
y  C_  ( ( int `  S ) `  s )  <->  ( u  i^i  ( B " K
) )  C_  (
( int `  S
) `  s )
) )
6261anbi1d 704 . . . . . . . . . . . 12  |-  ( y  =  ( u  i^i  ( B " K
) )  ->  (
( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp )  <->  ( (
u  i^i  ( B " K ) )  C_  ( ( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )
6360, 62anbi12d 710 . . . . . . . . . . 11  |-  ( y  =  ( u  i^i  ( B " K
) )  ->  (
( x  e.  y  /\  ( y  C_  ( ( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) )  <->  ( x  e.  ( u  i^i  ( B " K ) )  /\  ( ( u  i^i  ( B " K ) )  C_  ( ( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) ) )
6463rspcev 3073 . . . . . . . . . 10  |-  ( ( ( u  i^i  ( B " K ) )  e.  ( St  ( B
" K ) )  /\  ( x  e.  ( u  i^i  ( B " K ) )  /\  ( ( u  i^i  ( B " K ) )  C_  ( ( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )  ->  E. y  e.  ( St  ( B " K
) ) ( x  e.  y  /\  (
y  C_  ( ( int `  S ) `  s )  /\  ( St  s )  e.  Comp ) ) )
6543, 46, 59, 64syl12anc 1216 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  ( B " K ) )  /\  s  e.  ~P ( `' A " V ) )  /\  ( u  e.  S  /\  (
x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp ) ) )  ->  E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  ( y 
C_  ( ( int `  S ) `  s
)  /\  ( St  s
)  e.  Comp )
) )
6665rexlimdvaa 2842 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( B " K
) )  /\  s  e.  ~P ( `' A " V ) )  -> 
( E. u  e.  S  ( x  e.  u  /\  u  C_  s  /\  ( St  s )  e.  Comp )  ->  E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) ) )
6766reximdva 2828 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  ( E. s  e.  ~P  ( `' A " V ) E. u  e.  S  ( x  e.  u  /\  u  C_  s  /\  ( St  s )  e. 
Comp )  ->  E. s  e.  ~P  ( `' A " V ) E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) ) )
6834, 67mpd 15 . . . . . 6  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  E. s  e.  ~P  ( `' A " V ) E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )
69 rexcom 2882 . . . . . . 7  |-  ( E. s  e.  ~P  ( `' A " V ) E. y  e.  ( St  ( B " K
) ) ( x  e.  y  /\  (
y  C_  ( ( int `  S ) `  s )  /\  ( St  s )  e.  Comp ) )  <->  E. y  e.  ( St  ( B " K ) ) E. s  e.  ~P  ( `' A " V ) ( x  e.  y  /\  ( y  C_  ( ( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )
70 r19.42v 2875 . . . . . . . 8  |-  ( E. s  e.  ~P  ( `' A " V ) ( x  e.  y  /\  ( y  C_  ( ( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) )  <->  ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y 
C_  ( ( int `  S ) `  s
)  /\  ( St  s
)  e.  Comp )
) )
7170rexbii 2740 . . . . . . 7  |-  ( E. y  e.  ( St  ( B " K ) ) E. s  e. 
~P  ( `' A " V ) ( x  e.  y  /\  (
y  C_  ( ( int `  S ) `  s )  /\  ( St  s )  e.  Comp ) )  <->  E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )
7269, 71bitri 249 . . . . . 6  |-  ( E. s  e.  ~P  ( `' A " V ) E. y  e.  ( St  ( B " K
) ) ( x  e.  y  /\  (
y  C_  ( ( int `  S ) `  s )  /\  ( St  s )  e.  Comp ) )  <->  E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )
7368, 72sylib 196 . . . . 5  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )
7473ralrimiva 2799 . . . 4  |-  ( ph  ->  A. x  e.  ( B " K ) E. y  e.  ( St  ( B " K
) ) ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )
7515restuni 18766 . . . . . 6  |-  ( ( S  e.  Top  /\  ( B " K ) 
C_  U. S )  -> 
( B " K
)  =  U. ( St  ( B " K ) ) )
7636, 25, 75syl2anc 661 . . . . 5  |-  ( ph  ->  ( B " K
)  =  U. ( St  ( B " K ) ) )
7776raleqdv 2923 . . . 4  |-  ( ph  ->  ( A. x  e.  ( B " K
) E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) )  <->  A. x  e.  U. ( St  ( B
" K ) ) E. y  e.  ( St  ( B " K
) ) ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) ) )
7874, 77mpbid 210 . . 3  |-  ( ph  ->  A. x  e.  U. ( St  ( B " K ) ) E. y  e.  ( St  ( B " K ) ) ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y 
C_  ( ( int `  S ) `  s
)  /\  ( St  s
)  e.  Comp )
) )
79 eqid 2443 . . . 4  |-  U. ( St  ( B " K ) )  =  U. ( St  ( B " K ) )
80 fveq2 5691 . . . . . 6  |-  ( s  =  ( k `  y )  ->  (
( int `  S
) `  s )  =  ( ( int `  S ) `  (
k `  y )
) )
8180sseq2d 3384 . . . . 5  |-  ( s  =  ( k `  y )  ->  (
y  C_  ( ( int `  S ) `  s )  <->  y  C_  ( ( int `  S
) `  ( k `  y ) ) ) )
82 oveq2 6099 . . . . . 6  |-  ( s  =  ( k `  y )  ->  ( St  s )  =  ( St  ( k `  y
) ) )
8382eleq1d 2509 . . . . 5  |-  ( s  =  ( k `  y )  ->  (
( St  s )  e. 
Comp 
<->  ( St  ( k `  y ) )  e. 
Comp ) )
8481, 83anbi12d 710 . . . 4  |-  ( s  =  ( k `  y )  ->  (
( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp )  <->  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) )
8579, 84cmpcovf 18994 . . 3  |-  ( ( ( St  ( B " K ) )  e. 
Comp  /\  A. x  e. 
U. ( St  ( B
" K ) ) E. y  e.  ( St  ( B " K
) ) ( x  e.  y  /\  E. s  e.  ~P  ( `' A " V ) ( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp ) ) )  ->  E. w  e.  ( ~P ( St  ( B
" K ) )  i^i  Fin ) ( U. ( St  ( B
" K ) )  =  U. w  /\  E. k ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )
864, 78, 85syl2anc 661 . 2  |-  ( ph  ->  E. w  e.  ( ~P ( St  ( B
" K ) )  i^i  Fin ) ( U. ( St  ( B
" K ) )  =  U. w  /\  E. k ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )
8776adantr 465 . . . . . . 7  |-  ( (
ph  /\  w  e.  ( ~P ( St  ( B
" K ) )  i^i  Fin ) )  ->  ( B " K )  =  U. ( St  ( B " K ) ) )
8887eqeq1d 2451 . . . . . 6  |-  ( (
ph  /\  w  e.  ( ~P ( St  ( B
" K ) )  i^i  Fin ) )  ->  ( ( B
" K )  = 
U. w  <->  U. ( St  ( B " K ) )  =  U. w
) )
8988biimpar 485 . . . . 5  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  U. ( St  ( B " K ) )  =  U. w
)  ->  ( B " K )  =  U. w )
9036ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  S  e.  Top )
91 cntop2 18845 . . . . . . . . . . . 12  |-  ( A  e.  ( S  Cn  T )  ->  T  e.  Top )
927, 91syl 16 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  Top )
9392ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  T  e.  Top )
94 xkotop 19161 . . . . . . . . . 10  |-  ( ( S  e.  Top  /\  T  e.  Top )  ->  ( T  ^ko  S )  e.  Top )
9590, 93, 94syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( T  ^ko  S )  e.  Top )
96 cntop1 18844 . . . . . . . . . . . 12  |-  ( B  e.  ( R  Cn  S )  ->  R  e.  Top )
971, 96syl 16 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  Top )
9897ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  R  e.  Top )
99 xkotop 19161 . . . . . . . . . 10  |-  ( ( R  e.  Top  /\  S  e.  Top )  ->  ( S  ^ko  R )  e.  Top )
10098, 90, 99syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( S  ^ko  R )  e.  Top )
101 simprrl 763 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  k :
w --> ~P ( `' A " V ) )
102 frn 5565 . . . . . . . . . . . . 13  |-  ( k : w --> ~P ( `' A " V )  ->  ran  k  C_  ~P ( `' A " V ) )
103101, 102syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ran  k  C_  ~P ( `' A " V ) )
104 sspwuni 4256 . . . . . . . . . . . 12  |-  ( ran  k  C_  ~P ( `' A " V )  <->  U. ran  k  C_  ( `' A " V ) )
105103, 104sylib 196 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U. ran  k  C_  ( `' A " V ) )
10610ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( `' A " V )  e.  S )
107106, 50syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( `' A " V )  C_  U. S )
108105, 107sstrd 3366 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U. ran  k  C_ 
U. S )
109 ffn 5559 . . . . . . . . . . . . 13  |-  ( k : w --> ~P ( `' A " V )  ->  k  Fn  w
)
110 fniunfv 5964 . . . . . . . . . . . . 13  |-  ( k  Fn  w  ->  U_ y  e.  w  ( k `  y )  =  U. ran  k )
111101, 109, 1103syl 20 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  ( k `  y )  =  U. ran  k )
112111oveq2d 6107 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( St  U_ y  e.  w  ( k `  y ) )  =  ( St  U. ran  k ) )
113 inss2 3571 . . . . . . . . . . . . 13  |-  ( ~P ( St  ( B " K ) )  i^i 
Fin )  C_  Fin
114 simplr 754 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  w  e.  ( ~P ( St  ( B
" K ) )  i^i  Fin ) )
115113, 114sseldi 3354 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  w  e.  Fin )
116 simprrr 764 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) )
117 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( y  C_  ( ( int `  S ) `  ( k `  y
) )  /\  ( St  ( k `  y
) )  e.  Comp )  ->  ( St  ( k `
 y ) )  e.  Comp )
118117ralimi 2791 . . . . . . . . . . . . 13  |-  ( A. y  e.  w  (
y  C_  ( ( int `  S ) `  ( k `  y
) )  /\  ( St  ( k `  y
) )  e.  Comp )  ->  A. y  e.  w  ( St  ( k `  y ) )  e. 
Comp )
119116, 118syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  A. y  e.  w  ( St  (
k `  y )
)  e.  Comp )
12015fiuncmp 19007 . . . . . . . . . . . 12  |-  ( ( S  e.  Top  /\  w  e.  Fin  /\  A. y  e.  w  ( St  ( k `  y
) )  e.  Comp )  ->  ( St  U_ y  e.  w  ( k `  y ) )  e. 
Comp )
12190, 115, 119, 120syl3anc 1218 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( St  U_ y  e.  w  ( k `  y ) )  e. 
Comp )
122112, 121eqeltrrd 2518 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( St  U. ran  k )  e.  Comp )
1238ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  V  e.  T )
12415, 90, 93, 108, 122, 123xkoopn 19162 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  { a  e.  ( S  Cn  T
)  |  ( a
" U. ran  k
)  C_  V }  e.  ( T  ^ko  S ) )
125 xkococn.k . . . . . . . . . . 11  |-  ( ph  ->  K  C_  U. R )
126125ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  K  C_  U. R
)
1272ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( Rt  K
)  e.  Comp )
128111, 108eqsstrd 3390 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  ( k `  y )  C_  U. S
)
129 iunss 4211 . . . . . . . . . . . . 13  |-  ( U_ y  e.  w  (
k `  y )  C_ 
U. S  <->  A. y  e.  w  ( k `  y )  C_  U. S
)
130128, 129sylib 196 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  A. y  e.  w  ( k `  y )  C_  U. S
)
13115ntropn 18653 . . . . . . . . . . . . . 14  |-  ( ( S  e.  Top  /\  ( k `  y
)  C_  U. S )  ->  ( ( int `  S ) `  (
k `  y )
)  e.  S )
132131ex 434 . . . . . . . . . . . . 13  |-  ( S  e.  Top  ->  (
( k `  y
)  C_  U. S  -> 
( ( int `  S
) `  ( k `  y ) )  e.  S ) )
133132ralimdv 2795 . . . . . . . . . . . 12  |-  ( S  e.  Top  ->  ( A. y  e.  w  ( k `  y
)  C_  U. S  ->  A. y  e.  w  ( ( int `  S
) `  ( k `  y ) )  e.  S ) )
13490, 130, 133sylc 60 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  A. y  e.  w  ( ( int `  S ) `  ( k `  y
) )  e.  S
)
135 iunopn 18511 . . . . . . . . . . 11  |-  ( ( S  e.  Top  /\  A. y  e.  w  ( ( int `  S
) `  ( k `  y ) )  e.  S )  ->  U_ y  e.  w  ( ( int `  S ) `  ( k `  y
) )  e.  S
)
13690, 134, 135syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
)  e.  S )
13721, 98, 90, 126, 127, 136xkoopn 19162 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  { b  e.  ( R  Cn  S
)  |  ( b
" K )  C_  U_ y  e.  w  ( ( int `  S
) `  ( k `  y ) ) }  e.  ( S  ^ko  R ) )
138 txopn 19175 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
13995, 100, 124, 137, 138syl22anc 1219 . . . . . . . 8  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 ) ) )
1407ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  A  e.  ( S  Cn  T
) )
141 imaiun 5962 . . . . . . . . . . . 12  |-  ( A
" U_ y  e.  w  ( k `  y
) )  =  U_ y  e.  w  ( A " ( k `  y ) )
142111imaeq2d 5169 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( A "
U_ y  e.  w  ( k `  y
) )  =  ( A " U. ran  k ) )
143141, 142syl5eqr 2489 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  ( A "
( k `  y
) )  =  ( A " U. ran  k ) )
144111, 105eqsstrd 3390 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  ( k `  y )  C_  ( `' A " V ) )
14519ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  Fun  A )
146101, 109syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  k  Fn  w )
14727ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  dom  A  = 
U. S )
148108, 147sseqtr4d 3393 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U. ran  k  C_ 
dom  A )
149 simpl1 991 . . . . . . . . . . . . . . . 16  |-  ( ( ( Fun  A  /\  k  Fn  w  /\  U.
ran  k  C_  dom  A )  /\  y  e.  w )  ->  Fun  A )
1501103ad2ant2 1010 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  A  /\  k  Fn  w  /\  U. ran  k  C_  dom  A )  ->  U_ y  e.  w  ( k `  y
)  =  U. ran  k )
151 simp3 990 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  A  /\  k  Fn  w  /\  U. ran  k  C_  dom  A )  ->  U. ran  k  C_  dom  A )
152150, 151eqsstrd 3390 . . . . . . . . . . . . . . . . . 18  |-  ( ( Fun  A  /\  k  Fn  w  /\  U. ran  k  C_  dom  A )  ->  U_ y  e.  w  ( k `  y
)  C_  dom  A )
153 iunss 4211 . . . . . . . . . . . . . . . . . 18  |-  ( U_ y  e.  w  (
k `  y )  C_ 
dom  A  <->  A. y  e.  w  ( k `  y
)  C_  dom  A )
154152, 153sylib 196 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  A  /\  k  Fn  w  /\  U. ran  k  C_  dom  A )  ->  A. y  e.  w  ( k `  y
)  C_  dom  A )
155154r19.21bi 2814 . . . . . . . . . . . . . . . 16  |-  ( ( ( Fun  A  /\  k  Fn  w  /\  U.
ran  k  C_  dom  A )  /\  y  e.  w )  ->  (
k `  y )  C_ 
dom  A )
156 funimass3 5819 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  A  /\  (
k `  y )  C_ 
dom  A )  -> 
( ( A "
( k `  y
) )  C_  V  <->  ( k `  y ) 
C_  ( `' A " V ) ) )
157149, 155, 156syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( Fun  A  /\  k  Fn  w  /\  U.
ran  k  C_  dom  A )  /\  y  e.  w )  ->  (
( A " (
k `  y )
)  C_  V  <->  ( k `  y )  C_  ( `' A " V ) ) )
158157ralbidva 2731 . . . . . . . . . . . . . 14  |-  ( ( 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 4211 . . . . . . . . . . . . . 14  |-  ( U_ y  e.  w  ( A " ( k `  y ) )  C_  V 
<-> 
A. y  e.  w  ( A " ( k `
 y ) ) 
C_  V )
160 iunss 4211 . . . . . . . . . . . . . 14  |-  ( U_ y  e.  w  (
k `  y )  C_  ( `' A " V )  <->  A. y  e.  w  ( k `  y )  C_  ( `' A " V ) )
161158, 159, 1603bitr4g 288 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) )
162145, 146, 148, 161syl3anc 1218 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( U_ y  e.  w  ( A " ( k `  y ) )  C_  V 
<-> 
U_ y  e.  w  ( k `  y
)  C_  ( `' A " V ) ) )
163144, 162mpbird 232 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  ( A "
( k `  y
) )  C_  V
)
164143, 163eqsstr3d 3391 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( A " U. ran  k ) 
C_  V )
165 imaeq1 5164 . . . . . . . . . . . 12  |-  ( a  =  A  ->  (
a " U. ran  k )  =  ( A " U. ran  k ) )
166165sseq1d 3383 . . . . . . . . . . 11  |-  ( a  =  A  ->  (
( a " U. ran  k )  C_  V  <->  ( A " U. ran  k )  C_  V
) )
167166elrab 3117 . . . . . . . . . 10  |-  ( A  e.  { a  e.  ( S  Cn  T
)  |  ( a
" U. ran  k
)  C_  V }  <->  ( A  e.  ( S  Cn  T )  /\  ( A " U. ran  k )  C_  V
) )
168140, 164, 167sylanbrc 664 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  A  e.  { a  e.  ( S  Cn  T )  |  ( a " U. ran  k )  C_  V } )
1691ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  B  e.  ( R  Cn  S
) )
170 simprl 755 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( B " K )  =  U. w )
171 uniiun 4223 . . . . . . . . . . . 12  |-  U. w  =  U_ y  e.  w  y
172170, 171syl6eq 2491 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( B " K )  =  U_ y  e.  w  y
)
173 simpl 457 . . . . . . . . . . . . 13  |-  ( ( y  C_  ( ( int `  S ) `  ( k `  y
) )  /\  ( St  ( k `  y
) )  e.  Comp )  ->  y  C_  (
( int `  S
) `  ( k `  y ) ) )
174173ralimi 2791 . . . . . . . . . . . 12  |-  ( A. y  e.  w  (
y  C_  ( ( int `  S ) `  ( k `  y
) )  /\  ( St  ( k `  y
) )  e.  Comp )  ->  A. y  e.  w  y  C_  ( ( int `  S ) `  (
k `  y )
) )
175 ss2iun 4186 . . . . . . . . . . . 12  |-  ( A. y  e.  w  y  C_  ( ( int `  S
) `  ( k `  y ) )  ->  U_ y  e.  w  y  C_  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
) )
176116, 174, 1753syl 20 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  y  C_  U_ y  e.  w  ( ( int `  S ) `  ( k `  y
) ) )
177172, 176eqsstrd 3390 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  ( B " K )  C_  U_ y  e.  w  ( ( int `  S ) `  ( k `  y
) ) )
178 imaeq1 5164 . . . . . . . . . . . 12  |-  ( b  =  B  ->  (
b " K )  =  ( B " K ) )
179178sseq1d 3383 . . . . . . . . . . 11  |-  ( b  =  B  ->  (
( b " K
)  C_  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
)  <->  ( B " K )  C_  U_ y  e.  w  ( ( int `  S ) `  ( k `  y
) ) ) )
180179elrab 3117 . . . . . . . . . 10  |-  ( B  e.  { b  e.  ( R  Cn  S
)  |  ( b
" K )  C_  U_ y  e.  w  ( ( int `  S
) `  ( k `  y ) ) }  <-> 
( B  e.  ( R  Cn  S )  /\  ( B " K )  C_  U_ y  e.  w  ( ( int `  S ) `  ( k `  y
) ) ) )
181169, 177, 180sylanbrc 664 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  B  e.  { b  e.  ( R  Cn  S )  |  ( b " K
)  C_  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
) } )
182 opelxpi 4871 . . . . . . . . 9  |-  ( ( A  e.  { a  e.  ( S  Cn  T )  |  ( a " U. ran  k )  C_  V }  /\  B  e.  {
b  e.  ( R  Cn  S )  |  ( b " K
)  C_  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
) } )  ->  <. 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
) ) } ) )
183168, 181, 182syl2anc 661 . . . . . . . 8  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 ) ) } ) )
184 imaeq1 5164 . . . . . . . . . . . . . . 15  |-  ( a  =  u  ->  (
a " U. ran  k )  =  ( u " U. ran  k ) )
185184sseq1d 3383 . . . . . . . . . . . . . 14  |-  ( a  =  u  ->  (
( a " U. ran  k )  C_  V  <->  ( u " U. ran  k )  C_  V
) )
186185elrab 3117 . . . . . . . . . . . . 13  |-  ( u  e.  { a  e.  ( S  Cn  T
)  |  ( a
" U. ran  k
)  C_  V }  <->  ( u  e.  ( S  Cn  T )  /\  ( u " U. ran  k )  C_  V
) )
187 imaeq1 5164 . . . . . . . . . . . . . . 15  |-  ( b  =  v  ->  (
b " K )  =  ( v " K ) )
188187sseq1d 3383 . . . . . . . . . . . . . 14  |-  ( b  =  v  ->  (
( b " K
)  C_  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
)  <->  ( v " K )  C_  U_ y  e.  w  ( ( int `  S ) `  ( k `  y
) ) ) )
189188elrab 3117 . . . . . . . . . . . . 13  |-  ( 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
) ) ) )
190186, 189anbi12i 697 . . . . . . . . . . . 12  |-  ( ( 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
) ) ) ) )
191 simprll 761 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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
) )
192 simprrl 763 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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
) )
193 coeq1 4997 . . . . . . . . . . . . . . 15  |-  ( f  =  u  ->  (
f  o.  g )  =  ( u  o.  g ) )
194 coeq2 4998 . . . . . . . . . . . . . . 15  |-  ( g  =  v  ->  (
u  o.  g )  =  ( u  o.  v ) )
195 xkococn.1 . . . . . . . . . . . . . . 15  |-  F  =  ( f  e.  ( S  Cn  T ) ,  g  e.  ( R  Cn  S ) 
|->  ( f  o.  g
) )
196 vex 2975 . . . . . . . . . . . . . . . 16  |-  u  e. 
_V
197 vex 2975 . . . . . . . . . . . . . . . 16  |-  v  e. 
_V
198196, 197coex 6529 . . . . . . . . . . . . . . 15  |-  ( u  o.  v )  e. 
_V
199193, 194, 195, 198ovmpt2 6226 . . . . . . . . . . . . . 14  |-  ( ( u  e.  ( S  Cn  T )  /\  v  e.  ( R  Cn  S ) )  -> 
( u F v )  =  ( u  o.  v ) )
200191, 192, 199syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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
) )
201 cnco 18870 . . . . . . . . . . . . . . 15  |-  ( ( v  e.  ( R  Cn  S )  /\  u  e.  ( S  Cn  T ) )  -> 
( u  o.  v
)  e.  ( R  Cn  T ) )
202192, 191, 201syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 ) )
203 imaco 5343 . . . . . . . . . . . . . . 15  |-  ( ( u  o.  v )
" K )  =  ( u " (
v " K ) )
204 simprrr 764 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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
) ) )
20515ntrss2 18661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( S  e.  Top  /\  ( k `  y
)  C_  U. S )  ->  ( ( int `  S ) `  (
k `  y )
)  C_  ( k `  y ) )
206205ex 434 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S  e.  Top  ->  (
( k `  y
)  C_  U. S  -> 
( ( int `  S
) `  ( k `  y ) )  C_  ( k `  y
) ) )
207206ralimdv 2795 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( S  e.  Top  ->  ( A. y  e.  w  ( k `  y
)  C_  U. S  ->  A. y  e.  w  ( ( int `  S
) `  ( k `  y ) )  C_  ( k `  y
) ) )
20890, 130, 207sylc 60 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  A. y  e.  w  ( ( int `  S ) `  ( k `  y
) )  C_  (
k `  y )
)
209 ss2iun 4186 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) )
210208, 209syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
)  C_  U_ y  e.  w  ( k `  y ) )
211210, 111sseqtrd 3392 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) ) )  ->  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
)  C_  U. ran  k
)
212211adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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
)
213204, 212sstrd 3366 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 )
214 imass2 5204 . . . . . . . . . . . . . . . . 17  |-  ( ( v " K ) 
C_  U. ran  k  -> 
( u " (
v " K ) )  C_  ( u " U. ran  k ) )
215213, 214syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 ) )
216 simprlr 762 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 )
217215, 216sstrd 3366 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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
)
218203, 217syl5eqss 3400 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 )
219 imaeq1 5164 . . . . . . . . . . . . . . . 16  |-  ( h  =  ( u  o.  v )  ->  (
h " K )  =  ( ( u  o.  v ) " K ) )
220219sseq1d 3383 . . . . . . . . . . . . . . 15  |-  ( h  =  ( u  o.  v )  ->  (
( h " K
)  C_  V  <->  ( (
u  o.  v )
" K )  C_  V ) )
221220elrab 3117 . . . . . . . . . . . . . 14  |-  ( ( u  o.  v )  e.  { h  e.  ( R  Cn  T
)  |  ( h
" K )  C_  V }  <->  ( ( u  o.  v )  e.  ( R  Cn  T
)  /\  ( (
u  o.  v )
" K )  C_  V ) )
222202, 218, 221sylanbrc 664 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 }
)
223200, 222eqeltrd 2517 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 } )
224190, 223sylan2b 475 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i 
Fin ) )  /\  ( ( B " K )  =  U. w  /\  ( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 } )
225224ralrimivva 2808 . . . . . . . . . 10  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 } )
226195mpt2fun 6192 . . . . . . . . . . 11  |-  Fun  F
227 ssrab2 3437 . . . . . . . . . . . . 13  |-  { a  e.  ( S  Cn  T )  |  ( a " U. ran  k )  C_  V }  C_  ( S  Cn  T )
228 ssrab2 3437 . . . . . . . . . . . . 13  |-  { b  e.  ( R  Cn  S )  |  ( b " K ) 
C_  U_ y  e.  w  ( ( int `  S
) `  ( k `  y ) ) } 
C_  ( R  Cn  S )
229 xpss12 4945 . . . . . . . . . . . . 13  |-  ( ( { 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
) ) )
230227, 228, 229mp2an 672 . . . . . . . . . . . 12  |-  ( { 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
) )
231 vex 2975 . . . . . . . . . . . . . 14  |-  f  e. 
_V
232 vex 2975 . . . . . . . . . . . . . 14  |-  g  e. 
_V
233231, 232coex 6529 . . . . . . . . . . . . 13  |-  ( f  o.  g )  e. 
_V
234195, 233dmmpt2 6644 . . . . . . . . . . . 12  |-  dom  F  =  ( ( S  Cn  T )  X.  ( R  Cn  S
) )
235230, 234sseqtr4i 3389 . . . . . . . . . . 11  |-  ( { 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
236 funimassov 6240 . . . . . . . . . . 11  |-  ( ( 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 } ) )
237226, 235, 236mp2an 672 . . . . . . . . . 10  |-  ( ( 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 } )
238225, 237sylibr 212 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 } )
239 funimass3 5819 . . . . . . . . . 10  |-  ( ( 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 } ) ) )
240226, 235, 239mp2an 672 . . . . . . . . 9  |-  ( ( 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 } ) )
241238, 240sylib 196 . . . . . . . 8  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 } ) )
242 eleq2 2504 . . . . . . . . . 10  |-  ( 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
) ) } ) ) )
243 sseq1 3377 . . . . . . . . . 10  |-  ( 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 } ) ) )
244242, 243anbi12d 710 . . . . . . . . 9  |-  ( 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 } ) ) ) )
245244rspcev 3073 . . . . . . . 8  |-  ( ( ( { 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 } ) ) )
246139, 183, 241, 245syl12anc 1216 . . . . . . 7  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( ( B " K )  = 
U. w  /\  (
k : w --> ~P ( `' A " V )  /\  A. y  e.  w  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( 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 } ) ) )
247246expr 615 . . . . . 6  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( B " K )  =  U. w )  ->  (
( k : w --> ~P ( `' A " V )  /\  A. y  e.  w  (
y  C_  ( ( int `  S ) `  ( k `  y
) )  /\  ( St  ( 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 } ) ) ) )
248247exlimdv 1690 . . . . 5  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( 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 ) )  /\  ( St  ( k `  y )