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

Theorem xkococnlem 17679
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  ^ k o  S )  tX  ( S  ^ k o  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 17448 . . . 4  |-  ( ( B  e.  ( R  Cn  S )  /\  ( Rt  K )  e.  Comp )  ->  ( St  ( B
" K ) )  e.  Comp )
41, 2, 3syl2anc 643 . . 3  |-  ( ph  ->  ( St  ( B " K ) )  e. 
Comp )
5 xkococn.s . . . . . . . . 9  |-  ( ph  ->  S  e. 𝑛Locally  Comp )
65adantr 452 . . . . . . . 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 17317 . . . . . . . . . 10  |-  ( ( A  e.  ( S  Cn  T )  /\  V  e.  T )  ->  ( `' A " V )  e.  S
)
107, 8, 9syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( `' A " V )  e.  S
)
1110adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  ( `' A " V )  e.  S )
12 imaco 5366 . . . . . . . . . . 11  |-  ( ( A  o.  B )
" K )  =  ( A " ( B " K ) )
13 xkococn.i . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  o.  B ) " K
)  C_  V )
1412, 13syl5eqssr 3385 . . . . . . . . . 10  |-  ( ph  ->  ( A " ( B " K ) ) 
C_  V )
15 eqid 2435 . . . . . . . . . . . . 13  |-  U. S  =  U. S
16 eqid 2435 . . . . . . . . . . . . 13  |-  U. T  =  U. T
1715, 16cnf 17298 . . . . . . . . . . . 12  |-  ( A  e.  ( S  Cn  T )  ->  A : U. S --> U. T
)
18 ffun 5584 . . . . . . . . . . . 12  |-  ( A : U. S --> U. T  ->  Fun  A )
197, 17, 183syl 19 . . . . . . . . . . 11  |-  ( ph  ->  Fun  A )
20 imassrn 5207 . . . . . . . . . . . . 13  |-  ( B
" K )  C_  ran  B
21 eqid 2435 . . . . . . . . . . . . . . 15  |-  U. R  =  U. R
2221, 15cnf 17298 . . . . . . . . . . . . . 14  |-  ( B  e.  ( R  Cn  S )  ->  B : U. R --> U. S
)
23 frn 5588 . . . . . . . . . . . . . 14  |-  ( B : U. R --> U. S  ->  ran  B  C_  U. S
)
241, 22, 233syl 19 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  B  C_  U. S
)
2520, 24syl5ss 3351 . . . . . . . . . . . 12  |-  ( ph  ->  ( B " K
)  C_  U. S )
26 fdm 5586 . . . . . . . . . . . . 13  |-  ( A : U. S --> U. T  ->  dom  A  =  U. S )
277, 17, 263syl 19 . . . . . . . . . . . 12  |-  ( ph  ->  dom  A  =  U. S )
2825, 27sseqtr4d 3377 . . . . . . . . . . 11  |-  ( ph  ->  ( B " K
)  C_  dom  A )
29 funimass3 5837 . . . . . . . . . . 11  |-  ( ( Fun  A  /\  ( B " K )  C_  dom  A )  ->  (
( A " ( B " K ) ) 
C_  V  <->  ( B " K )  C_  ( `' A " V ) ) )
3019, 28, 29syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( ( A "
( B " K
) )  C_  V  <->  ( B " K ) 
C_  ( `' A " V ) ) )
3114, 30mpbid 202 . . . . . . . . 9  |-  ( ph  ->  ( B " K
)  C_  ( `' A " V ) )
3231sselda 3340 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( B " K ) )  ->  x  e.  ( `' A " V ) )
33 nlly2i 17527 . . . . . . . 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 1184 . . . . . . 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 17524 . . . . . . . . . . . . 13  |-  ( S  e. 𝑛Locally 
Comp  ->  S  e.  Top )
365, 35syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  Top )
3736ad3antrrr 711 . . . . . . . . . . 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 5208 . . . . . . . . . . . . 13  |-  ( B  e.  ( R  Cn  S )  ->  ( B " K )  e. 
_V )
391, 38syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( B " K
)  e.  _V )
4039ad3antrrr 711 . . . . . . . . . . 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 733 . . . . . . . . . . 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 13644 . . . . . . . . . . 11  |-  ( ( S  e.  Top  /\  ( B " K )  e.  _V  /\  u  e.  S )  ->  (
u  i^i  ( B " K ) )  e.  ( St  ( B " K ) ) )
4337, 40, 41, 42syl3anc 1184 . . . . . . . . . 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 1005 . . . . . . . . . . 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 736 . . . . . . . . . . 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 ) )
46 elin 3522 . . . . . . . . . . 11  |-  ( x  e.  ( u  i^i  ( B " K
) )  <->  ( x  e.  u  /\  x  e.  ( B " K
) ) )
4744, 45, 46sylanbrc 646 . . . . . . . . . 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
) ) )
48 inss1 3553 . . . . . . . . . . . 12  |-  ( u  i^i  ( B " K ) )  C_  u
49 elpwi 3799 . . . . . . . . . . . . . . 15  |-  ( s  e.  ~P ( `' A " V )  ->  s  C_  ( `' A " V ) )
5049ad2antlr 708 . . . . . . . . . . . . . 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 ) )
51 elssuni 4035 . . . . . . . . . . . . . . . 16  |-  ( ( `' A " V )  e.  S  ->  ( `' A " V ) 
C_  U. S )
5210, 51syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( `' A " V )  C_  U. S
)
5352ad3antrrr 711 . . . . . . . . . . . . . 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
)
5450, 53sstrd 3350 . . . . . . . . . . . . 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 )
55 simprr2 1006 . . . . . . . . . . . . 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 )
5615ssntr 17110 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  Top  /\  s  C_  U. S )  /\  ( u  e.  S  /\  u  C_  s ) )  ->  u  C_  ( ( int `  S ) `  s
) )
5737, 54, 41, 55, 56syl22anc 1185 . . . . . . . . . . . 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
) )
5848, 57syl5ss 3351 . . . . . . . . . . 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
) )
59 simprr3 1007 . . . . . . . . . . 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 )
6058, 59jca 519 . . . . . . . . . 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 ) )
61 eleq2 2496 . . . . . . . . . . . 12  |-  ( y  =  ( u  i^i  ( B " K
) )  ->  (
x  e.  y  <->  x  e.  ( u  i^i  ( B " K ) ) ) )
62 sseq1 3361 . . . . . . . . . . . . 13  |-  ( y  =  ( u  i^i  ( B " K
) )  ->  (
y  C_  ( ( int `  S ) `  s )  <->  ( u  i^i  ( B " K
) )  C_  (
( int `  S
) `  s )
) )
6362anbi1d 686 . . . . . . . . . . . 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 ) ) )
6461, 63anbi12d 692 . . . . . . . . . . 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 ) ) ) )
6564rspcev 3044 . . . . . . . . . 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 ) ) )
6643, 47, 60, 65syl12anc 1182 . . . . . . . . 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 )
) )
6766rexlimdvaa 2823 . . . . . . . 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 ) ) ) )
6867reximdva 2810 . . . . . . 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 ) ) ) )
6934, 68mpd 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 ) ) )
70 rexcom 2861 . . . . . . 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 ) ) )
71 r19.42v 2854 . . . . . . . 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 )
) )
7271rexbii 2722 . . . . . . 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 ) ) )
7370, 72bitri 241 . . . . . 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 ) ) )
7469, 73sylib 189 . . . . 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 ) ) )
7574ralrimiva 2781 . . . 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 ) ) )
7615restuni 17214 . . . . . 6  |-  ( ( S  e.  Top  /\  ( B " K ) 
C_  U. S )  -> 
( B " K
)  =  U. ( St  ( B " K ) ) )
7736, 25, 76syl2anc 643 . . . . 5  |-  ( ph  ->  ( B " K
)  =  U. ( St  ( B " K ) ) )
7877raleqdv 2902 . . . 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 ) ) ) )
7975, 78mpbid 202 . . 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 )
) )
80 eqid 2435 . . . 4  |-  U. ( St  ( B " K ) )  =  U. ( St  ( B " K ) )
81 fveq2 5719 . . . . . 6  |-  ( s  =  ( k `  y )  ->  (
( int `  S
) `  s )  =  ( ( int `  S ) `  (
k `  y )
) )
8281sseq2d 3368 . . . . 5  |-  ( s  =  ( k `  y )  ->  (
y  C_  ( ( int `  S ) `  s )  <->  y  C_  ( ( int `  S
) `  ( k `  y ) ) ) )
83 oveq2 6080 . . . . . 6  |-  ( s  =  ( k `  y )  ->  ( St  s )  =  ( St  ( k `  y
) ) )
8483eleq1d 2501 . . . . 5  |-  ( s  =  ( k `  y )  ->  (
( St  s )  e. 
Comp 
<->  ( St  ( k `  y ) )  e. 
Comp ) )
8582, 84anbi12d 692 . . . 4  |-  ( s  =  ( k `  y )  ->  (
( y  C_  (
( int `  S
) `  s )  /\  ( St  s )  e. 
Comp )  <->  ( y  C_  ( ( int `  S
) `  ( k `  y ) )  /\  ( St  ( k `  y ) )  e. 
Comp ) ) )
8680, 85cmpcovf 17442 . . 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 ) ) ) )
874, 79, 86syl2anc 643 . 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 ) ) ) )
8877adantr 452 . . . . . . 7  |-  ( (
ph  /\  w  e.  ( ~P ( St  ( B
" K ) )  i^i  Fin ) )  ->  ( B " K )  =  U. ( St  ( B " K ) ) )
8988eqeq1d 2443 . . . . . 6  |-  ( (
ph  /\  w  e.  ( ~P ( St  ( B
" K ) )  i^i  Fin ) )  ->  ( ( B
" K )  = 
U. w  <->  U. ( St  ( B " K ) )  =  U. w
) )
9089biimpar 472 . . . . 5  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  U. ( St  ( B " K ) )  =  U. w
)  ->  ( B " K )  =  U. w )
9136ad2antrr 707 . . . . . . . . . 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 )
92 cntop2 17293 . . . . . . . . . . . 12  |-  ( A  e.  ( S  Cn  T )  ->  T  e.  Top )
937, 92syl 16 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  Top )
9493ad2antrr 707 . . . . . . . . . 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 )
95 xkotop 17608 . . . . . . . . . 10  |-  ( ( S  e.  Top  /\  T  e.  Top )  ->  ( T  ^ k o  S )  e.  Top )
9691, 94, 95syl2anc 643 . . . . . . . . 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  ^ k o  S )  e.  Top )
97 cntop1 17292 . . . . . . . . . . . 12  |-  ( B  e.  ( R  Cn  S )  ->  R  e.  Top )
981, 97syl 16 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  Top )
9998ad2antrr 707 . . . . . . . . . 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 )
100 xkotop 17608 . . . . . . . . . 10  |-  ( ( R  e.  Top  /\  S  e.  Top )  ->  ( S  ^ k o  R )  e.  Top )
10199, 91, 100syl2anc 643 . . . . . . . . 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  ^ k o  R )  e.  Top )
102 simprrl 741 . . . . . . . . . . . . 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 ) )
103 frn 5588 . . . . . . . . . . . . 13  |-  ( k : w --> ~P ( `' A " V )  ->  ran  k  C_  ~P ( `' A " V ) )
104102, 103syl 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 ) )
105 sspwuni 4168 . . . . . . . . . . . 12  |-  ( ran  k  C_  ~P ( `' A " V )  <->  U. ran  k  C_  ( `' A " V ) )
106104, 105sylib 189 . . . . . . . . . . 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 ) )
10710ad2antrr 707 . . . . . . . . . . . 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 )
108107, 51syl 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 )
109106, 108sstrd 3350 . . . . . . . . . 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 )
110 ffn 5582 . . . . . . . . . . . . 13  |-  ( k : w --> ~P ( `' A " V )  ->  k  Fn  w
)
111 fniunfv 5985 . . . . . . . . . . . . 13  |-  ( k  Fn  w  ->  U_ y  e.  w  ( k `  y )  =  U. ran  k )
112102, 110, 1113syl 19 . . . . . . . . . . . 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 )
113112oveq2d 6088 . . . . . . . . . . 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 ) )
114 inss2 3554 . . . . . . . . . . . . 13  |-  ( ~P ( St  ( B " K ) )  i^i 
Fin )  C_  Fin
115 simplr 732 . . . . . . . . . . . . 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 ) )
116114, 115sseldi 3338 . . . . . . . . . . . 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 )
117 simprrr 742 . . . . . . . . . . . . 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 ) )
118 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( y  C_  ( ( int `  S ) `  ( k `  y
) )  /\  ( St  ( k `  y
) )  e.  Comp )  ->  ( St  ( k `
 y ) )  e.  Comp )
119118ralimi 2773 . . . . . . . . . . . . 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 )
120117, 119syl 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 )
12115fiuncmp 17455 . . . . . . . . . . . 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 )
12291, 116, 120, 121syl3anc 1184 . . . . . . . . . . 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 )
123113, 122eqeltrrd 2510 . . . . . . . . . 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 )
1248ad2antrr 707 . . . . . . . . . 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 )
12515, 91, 94, 109, 123, 124xkoopn 17609 . . . . . . . . 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  ^ k o  S ) )
126 xkococn.k . . . . . . . . . . 11  |-  ( ph  ->  K  C_  U. R )
127126ad2antrr 707 . . . . . . . . . 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
)
1282ad2antrr 707 . . . . . . . . . 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 )
129112, 109eqsstrd 3374 . . . . . . . . . . . . 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
)
130 iunss 4124 . . . . . . . . . . . . 13  |-  ( U_ y  e.  w  (
k `  y )  C_ 
U. S  <->  A. y  e.  w  ( k `  y )  C_  U. S
)
131129, 130sylib 189 . . . . . . . . . . . 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
)
13215ntropn 17101 . . . . . . . . . . . . . 14  |-  ( ( S  e.  Top  /\  ( k `  y
)  C_  U. S )  ->  ( ( int `  S ) `  (
k `  y )
)  e.  S )
133132ex 424 . . . . . . . . . . . . 13  |-  ( S  e.  Top  ->  (
( k `  y
)  C_  U. S  -> 
( ( int `  S
) `  ( k `  y ) )  e.  S ) )
134133ralimdv 2777 . . . . . . . . . . . 12  |-  ( S  e.  Top  ->  ( A. y  e.  w  ( k `  y
)  C_  U. S  ->  A. y  e.  w  ( ( int `  S
) `  ( k `  y ) )  e.  S ) )
13591, 131, 134sylc 58 . . . . . . . . . . 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
)
136 iunopn 16959 . . . . . . . . . . 11  |-  ( ( S  e.  Top  /\  A. y  e.  w  ( ( int `  S
) `  ( k `  y ) )  e.  S )  ->  U_ y  e.  w  ( ( int `  S ) `  ( k `  y
) )  e.  S
)
13791, 135, 136syl2anc 643 . . . . . . . . . 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 )
13821, 99, 91, 127, 128, 137xkoopn 17609 . . . . . . . . 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  ^ k o  R )
)
139 txopn 17622 . . . . . . . . 9  |-  ( ( ( ( T  ^ k o  S )  e.  Top  /\  ( S  ^ k o  R
)  e.  Top )  /\  ( { a  e.  ( S  Cn  T
)  |  ( a
" U. ran  k
)  C_  V }  e.  ( T  ^ k o  S )  /\  {
b  e.  ( R  Cn  S )  |  ( b " K
)  C_  U_ y  e.  w  ( ( int `  S ) `  (
k `  y )
) }  e.  ( S  ^ k o  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  ^ k o  S )  tX  ( S  ^ k o  R
) ) )
14096, 101, 125, 138, 139syl22anc 1185 . . . . . . . 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  ^ k o  S )  tX  ( S  ^ k o  R
) ) )
1417ad2antrr 707 . . . . . . . . . 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
) )
142 imaiun 5983 . . . . . . . . . . . 12  |-  ( A
" U_ y  e.  w  ( k `  y
) )  =  U_ y  e.  w  ( A " ( k `  y ) )
143112imaeq2d 5194 . . . . . . . . . . . 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 ) )
144142, 143syl5eqr 2481 . . . . . . . . . . 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 ) )
145112, 106eqsstrd 3374 . . . . . . . . . . . 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 ) )
14619ad2antrr 707 . . . . . . . . . . . . 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 )
147102, 110syl 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 )
14827ad2antrr 707 . . . . . . . . . . . . . 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 )
149109, 148sseqtr4d 3377 . . . . . . . . . . . . 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 )
150 simpl1 960 . . . . . . . . . . . . . . . 16  |-  ( ( ( Fun  A  /\  k  Fn  w  /\  U.
ran  k  C_  dom  A )  /\  y  e.  w )  ->  Fun  A )
1511113ad2ant2 979 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  A  /\  k  Fn  w  /\  U. ran  k  C_  dom  A )  ->  U_ y  e.  w  ( k `  y
)  =  U. ran  k )
152 simp3 959 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  A  /\  k  Fn  w  /\  U. ran  k  C_  dom  A )  ->  U. ran  k  C_  dom  A )
153151, 152eqsstrd 3374 . . . . . . . . . . . . . . . . . 18  |-  ( ( Fun  A  /\  k  Fn  w  /\  U. ran  k  C_  dom  A )  ->  U_ y  e.  w  ( k `  y
)  C_  dom  A )
154 iunss 4124 . . . . . . . . . . . . . . . . . 18  |-  ( U_ y  e.  w  (
k `  y )  C_ 
dom  A  <->  A. y  e.  w  ( k `  y
)  C_  dom  A )
155153, 154sylib 189 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  A  /\  k  Fn  w  /\  U. ran  k  C_  dom  A )  ->  A. y  e.  w  ( k `  y
)  C_  dom  A )
156155r19.21bi 2796 . . . . . . . . . . . . . . . 16  |-  ( ( ( Fun  A  /\  k  Fn  w  /\  U.
ran  k  C_  dom  A )  /\  y  e.  w )  ->  (
k `  y )  C_ 
dom  A )
157 funimass3 5837 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  A  /\  (
k `  y )  C_ 
dom  A )  -> 
( ( A "
( k `  y
) )  C_  V  <->  ( k `  y ) 
C_  ( `' A " V ) ) )
158150, 156, 157syl2anc 643 . . . . . . . . . . . . . . 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 ) ) )
159158ralbidva 2713 . . . . . . . . . . . . . 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 ) ) )
160 iunss 4124 . . . . . . . . . . . . . 14  |-  ( U_ y  e.  w  ( A " ( k `  y ) )  C_  V 
<-> 
A. y  e.  w  ( A " ( k `
 y ) ) 
C_  V )
161 iunss 4124 . . . . . . . . . . . . . 14  |-  ( U_ y  e.  w  (
k `  y )  C_  ( `' A " V )  <->  A. y  e.  w  ( k `  y )  C_  ( `' A " V ) )
162159, 160, 1613bitr4g 280 . . . . . . . . . . . . 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 ) ) )
163146, 147, 149, 162syl3anc 1184 . . . . . . . . . . . 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 ) ) )
164145, 163mpbird 224 . . . . . . . . . . 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
)
165144, 164eqsstr3d 3375 . . . . . . . . . 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 )
166 imaeq1 5189 . . . . . . . . . . . 12  |-  ( a  =  A  ->  (
a " U. ran  k )  =  ( A " U. ran  k ) )
167166sseq1d 3367 . . . . . . . . . . 11  |-  ( a  =  A  ->  (
( a " U. ran  k )  C_  V  <->  ( A " U. ran  k )  C_  V
) )
168167elrab 3084 . . . . . . . . . 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
) )
169141, 165, 168sylanbrc 646 . . . . . . . . 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 } )
1701ad2antrr 707 . . . . . . . . . 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
) )
171 simprl 733 . . . . . . . . . . . 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 )
172 uniiun 4136 . . . . . . . . . . . 12  |-  U. w  =  U_ y  e.  w  y
173171, 172syl6eq 2483 . . . . . . . . . . 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
)
174 simpl 444 . . . . . . . . . . . . 13  |-  ( ( y  C_  ( ( int `  S ) `  ( k `  y
) )  /\  ( St  ( k `  y
) )  e.  Comp )  ->  y  C_  (
( int `  S
) `  ( k `  y ) ) )
175174ralimi 2773 . . . . . . . . . . . 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 )
) )
176 ss2iun 4100 . . . . . . . . . . . 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 )
) )
177117, 175, 1763syl 19 . . . . . . . . . . 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
) ) )
178173, 177eqsstrd 3374 . . . . . . . . . 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
) ) )
179 imaeq1 5189 . . . . . . . . . . . 12  |-  ( b  =  B  ->  (
b " K )  =  ( B " K ) )
180179sseq1d 3367 . . . . . . . . . . 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
) ) ) )
181180elrab 3084 . . . . . . . . . 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
) ) ) )
182170, 178, 181sylanbrc 646 . . . . . . . . 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 )
) } )
183 opelxpi 4901 . . . . . . . . 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
) ) } ) )
184169, 182, 183syl2anc 643 . . . . . . . 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 ) ) } ) )
185 imaeq1 5189 . . . . . . . . . . . . . . 15  |-  ( a  =  u  ->  (
a " U. ran  k )  =  ( u " U. ran  k ) )
186185sseq1d 3367 . . . . . . . . . . . . . 14  |-  ( a  =  u  ->  (
( a " U. ran  k )  C_  V  <->  ( u " U. ran  k )  C_  V
) )
187186elrab 3084 . . . . . . . . . . . . 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
) )
188 imaeq1 5189 . . . . . . . . . . . . . . 15  |-  ( b  =  v  ->  (
b " K )  =  ( v " K ) )
189188sseq1d 3367 . . . . . . . . . . . . . 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
) ) ) )
190189elrab 3084 . . . . . . . . . . . . 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
) ) ) )
191187, 190anbi12i 679 . . . . . . . . . . . 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
) ) ) ) )
192 simprll 739 . . . . . . . . . . . . . 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
) )
193 simprrl 741 . . . . . . . . . . . . . 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
) )
194 coeq1 5021 . . . . . . . . . . . . . . 15  |-  ( f  =  u  ->  (
f  o.  g )  =  ( u  o.  g ) )
195 coeq2 5022 . . . . . . . . . . . . . . 15  |-  ( g  =  v  ->  (
u  o.  g )  =  ( u  o.  v ) )
196 xkococn.1 . . . . . . . . . . . . . . 15  |-  F  =  ( f  e.  ( S  Cn  T ) ,  g  e.  ( R  Cn  S ) 
|->  ( f  o.  g
) )
197 vex 2951 . . . . . . . . . . . . . . . 16  |-  u  e. 
_V
198 vex 2951 . . . . . . . . . . . . . . . 16  |-  v  e. 
_V
199197, 198coex 5404 . . . . . . . . . . . . . . 15  |-  ( u  o.  v )  e. 
_V
200194, 195, 196, 199ovmpt2 6200 . . . . . . . . . . . . . 14  |-  ( ( u  e.  ( S  Cn  T )  /\  v  e.  ( R  Cn  S ) )  -> 
( u F v )  =  ( u  o.  v ) )
201192, 193, 200syl2anc 643 . . . . . . . . . . . . 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
) )
202 cnco 17318 . . . . . . . . . . . . . . 15  |-  ( ( v  e.  ( R  Cn  S )  /\  u  e.  ( S  Cn  T ) )  -> 
( u  o.  v
)  e.  ( R  Cn  T ) )
203193, 192, 202syl2anc 643 . . . . . . . . . . . . . 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 ) )
204 imaco 5366 . . . . . . . . . . . . . . 15  |-  ( ( u  o.  v )
" K )  =  ( u " (
v " K ) )
205 simprrr 742 . . . . . . . . . . . . . . . . . 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
) ) )
20615ntrss2 17109 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( S  e.  Top  /\  ( k `  y
)  C_  U. S )  ->  ( ( int `  S ) `  (
k `  y )
)  C_  ( k `  y ) )
207206ex 424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( S  e.  Top  ->  (
( k `  y
)  C_  U. S  -> 
( ( int `  S
) `  ( k `  y ) )  C_  ( k `  y
) ) )
208207ralimdv 2777 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( S  e.  Top  ->  ( A. y  e.  w  ( k `  y
)  C_  U. S  ->  A. y  e.  w  ( ( int `  S
) `  ( k `  y ) )  C_  ( k `  y
) ) )
20991, 131, 208sylc 58 . . . . . . . . . . . . . . . . . . . . 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 )
)
210 ss2iun 4100 . . . . . . . . . . . . . . . . . . . . 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 ) )
211209, 210syl 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 ) )
212211, 112sseqtrd 3376 . . . . . . . . . . . . . . . . . . 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
)
213212adantr 452 . . . . . . . . . . . . . . . . . 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
)
214205, 213sstrd 3350 . . . . . . . . . . . . . . . . 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 )
215 imass2 5231 . . . . . . . . . . . . . . . . 17  |-  ( ( v " K ) 
C_  U. ran  k  -> 
( u " (
v " K ) )  C_  ( u " U. ran  k ) )
216214, 215syl 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 ) )
217 simprlr 740 . . . . . . . . . . . . . . . 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 )
218216, 217sstrd 3350 . . . . . . . . . . . . . . 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
)
219204, 218syl5eqss 3384 . . . . . . . . . . . . . 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 )
220 imaeq1 5189 . . . . . . . . . . . . . . . 16  |-  ( h  =  ( u  o.  v )  ->  (
h " K )  =  ( ( u  o.  v ) " K ) )
221220sseq1d 3367 . . . . . . . . . . . . . . 15  |-  ( h  =  ( u  o.  v )  ->  (
( h " K
)  C_  V  <->  ( (
u  o.  v )
" K )  C_  V ) )
222221elrab 3084 . . . . . . . . . . . . . 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 ) )
223203, 219, 222sylanbrc 646 . . . . . . . . . . . . 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 }
)
224201, 223eqeltrd 2509 . . . . . . . . . . . 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 } )
225191, 224sylan2b 462 . . . . . . . . . . 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 } )
226225ralrimivva 2790 . . . . . . . . . 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 } )
227196mpt2fun 6163 . . . . . . . . . . 11  |-  Fun  F
228 ssrab2 3420 . . . . . . . . . . . . 13  |-  { a  e.  ( S  Cn  T )  |  ( a " U. ran  k )  C_  V }  C_  ( S  Cn  T )
229 ssrab2 3420 . . . . . . . . . . . . 13  |-  { b  e.  ( R  Cn  S )  |  ( b " K ) 
C_  U_ y  e.  w  ( ( int `  S
) `  ( k `  y ) ) } 
C_  ( R  Cn  S )
230 xpss12 4972 . . . . . . . . . . . . 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
) ) )
231228, 229, 230mp2an 654 . . . . . . . . . . . 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
) )
232 vex 2951 . . . . . . . . . . . . . 14  |-  f  e. 
_V
233 vex 2951 . . . . . . . . . . . . . 14  |-  g  e. 
_V
234232, 233coex 5404 . . . . . . . . . . . . 13  |-  ( f  o.  g )  e. 
_V
235196, 234dmmpt2 6412 . . . . . . . . . . . 12  |-  dom  F  =  ( ( S  Cn  T )  X.  ( R  Cn  S
) )
236231, 235sseqtr4i 3373 . . . . . . . . . . 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
237 funimassov 6214 . . . . . . . . . . 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 } ) )
238227, 236, 237mp2an 654 . . . . . . . . . 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 } )
239226, 238sylibr 204 . . . . . . . . 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 } )
240 funimass3 5837 . . . . . . . . . 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 } ) ) )
241227, 236, 240mp2an 654 . . . . . . . . 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 } ) )
242239, 241sylib 189 . . . . . . . 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 } ) )
243 eleq2 2496 . . . . . . . . . 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
) ) } ) ) )
244 sseq1 3361 . . . . . . . . . 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 } ) ) )
245243, 244anbi12d 692 . . . . . . . . 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 } ) ) ) )
246245rspcev 3044 . . . . . . . 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  ^ k o  S
)  tX  ( S  ^ k o  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  ^ k o  S )  tX  ( S  ^ k o  R
) ) ( <. A ,  B >.  e.  z  /\  z  C_  ( `' F " { h  e.  ( R  Cn  T
)  |  ( h
" K )  C_  V } ) ) )
247140, 184, 242, 246syl12anc 1182 . . . . . . 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  ^ k o  S )  tX  ( S  ^ k o  R ) ) (
<. A ,  B >.  e.  z  /\  z  C_  ( `' F " { h  e.  ( R  Cn  T
)  |  ( h
" K )  C_  V } ) ) )
248247expr 599 . . . . . 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  ^ k o  S )  tX  ( S  ^ k o  R ) ) (
<. A ,  B >.  e.  z  /\  z  C_  ( `' F " { h  e.  ( R  Cn  T
)  |  ( h
" K )  C_  V } ) ) ) )
249248exlimdv 1646 . . . . 5  |-  ( ( ( ph  /\  w  e.  ( ~P ( St  ( B " K ) )  i^i  Fin )
)  /\  ( B " K )  =  U. w )  ->  ( E. k ( k : w --> ~P ( `' A