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

Theorem xkoco1cn 19230
Description: If  F is a continuous function, then  g  |->  g  o.  F is a continuous function on function spaces. (The reason we prove this and xkoco2cn 19231 independently of the more general xkococn 19233 is because that requires some inconvenient extra assumptions on  S.) (Contributed by Mario Carneiro, 20-Mar-2015.)
Hypotheses
Ref Expression
xkoco1cn.t  |-  ( ph  ->  T  e.  Top )
xkoco1cn.f  |-  ( ph  ->  F  e.  ( R  Cn  S ) )
Assertion
Ref Expression
xkoco1cn  |-  ( ph  ->  ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) )  e.  ( ( T  ^ko  S )  Cn  ( T  ^ko  R ) ) )
Distinct variable groups:    ph, g    R, g    S, g    T, g   
g, F

Proof of Theorem xkoco1cn
Dummy variables  k 
v  x  h  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkoco1cn.f . . . 4  |-  ( ph  ->  F  e.  ( R  Cn  S ) )
2 cnco 18870 . . . 4  |-  ( ( F  e.  ( R  Cn  S )  /\  g  e.  ( S  Cn  T ) )  -> 
( g  o.  F
)  e.  ( R  Cn  T ) )
31, 2sylan 471 . . 3  |-  ( (
ph  /\  g  e.  ( S  Cn  T
) )  ->  (
g  o.  F )  e.  ( R  Cn  T ) )
4 eqid 2443 . . 3  |-  ( g  e.  ( S  Cn  T )  |->  ( g  o.  F ) )  =  ( g  e.  ( S  Cn  T
)  |->  ( g  o.  F ) )
53, 4fmptd 5867 . 2  |-  ( ph  ->  ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) ) : ( S  Cn  T ) --> ( R  Cn  T
) )
6 eqid 2443 . . . . . 6  |-  U. R  =  U. R
7 eqid 2443 . . . . . 6  |-  { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp }  =  {
y  e.  ~P U. R  |  ( Rt  y
)  e.  Comp }
8 eqid 2443 . . . . . 6  |-  ( k  e.  { y  e. 
~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h "
k )  C_  v } )  =  ( k  e.  { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } )
96, 7, 8xkobval 19159 . . . . 5  |-  ran  (
k  e.  { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } )  =  {
x  |  E. k  e.  ~P  U. R E. v  e.  T  (
( Rt  k )  e. 
Comp  /\  x  =  {
h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
) }
109abeq2i 2550 . . . 4  |-  ( x  e.  ran  ( k  e.  { y  e. 
~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h "
k )  C_  v } )  <->  E. k  e.  ~P  U. R E. v  e.  T  (
( Rt  k )  e. 
Comp  /\  x  =  {
h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
) )
111ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  F  e.  ( R  Cn  S ) )
1211, 2sylan 471 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( k  e.  ~P U. R  /\  v  e.  T ) )  /\  ( Rt  k )  e. 
Comp )  /\  g  e.  ( S  Cn  T
) )  ->  (
g  o.  F )  e.  ( R  Cn  T ) )
13 imaeq1 5164 . . . . . . . . . . . . 13  |-  ( h  =  ( g  o.  F )  ->  (
h " k )  =  ( ( g  o.  F ) "
k ) )
14 imaco 5343 . . . . . . . . . . . . 13  |-  ( ( g  o.  F )
" k )  =  ( g " ( F " k ) )
1513, 14syl6eq 2491 . . . . . . . . . . . 12  |-  ( h  =  ( g  o.  F )  ->  (
h " k )  =  ( g "
( F " k
) ) )
1615sseq1d 3383 . . . . . . . . . . 11  |-  ( h  =  ( g  o.  F )  ->  (
( h " k
)  C_  v  <->  ( g " ( F "
k ) )  C_  v ) )
1716elrab3 3118 . . . . . . . . . 10  |-  ( ( g  o.  F )  e.  ( R  Cn  T )  ->  (
( g  o.  F
)  e.  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v }  <->  ( g "
( F " k
) )  C_  v
) )
1812, 17syl 16 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( k  e.  ~P U. R  /\  v  e.  T ) )  /\  ( Rt  k )  e. 
Comp )  /\  g  e.  ( S  Cn  T
) )  ->  (
( g  o.  F
)  e.  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v }  <->  ( g "
( F " k
) )  C_  v
) )
1918rabbidva 2963 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  { g  e.  ( S  Cn  T
)  |  ( g  o.  F )  e. 
{ h  e.  ( R  Cn  T )  |  ( h "
k )  C_  v } }  =  {
g  e.  ( S  Cn  T )  |  ( g " ( F " k ) ) 
C_  v } )
20 eqid 2443 . . . . . . . . 9  |-  U. S  =  U. S
21 cntop2 18845 . . . . . . . . . . 11  |-  ( F  e.  ( R  Cn  S )  ->  S  e.  Top )
221, 21syl 16 . . . . . . . . . 10  |-  ( ph  ->  S  e.  Top )
2322ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  S  e.  Top )
24 xkoco1cn.t . . . . . . . . . 10  |-  ( ph  ->  T  e.  Top )
2524ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  T  e.  Top )
26 imassrn 5180 . . . . . . . . . 10  |-  ( F
" k )  C_  ran  F
276, 20cnf 18850 . . . . . . . . . . 11  |-  ( F  e.  ( R  Cn  S )  ->  F : U. R --> U. S
)
28 frn 5565 . . . . . . . . . . 11  |-  ( F : U. R --> U. S  ->  ran  F  C_  U. S
)
2911, 27, 283syl 20 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  ran  F  C_  U. S
)
3026, 29syl5ss 3367 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  ( F "
k )  C_  U. S
)
31 imacmp 19000 . . . . . . . . . 10  |-  ( ( F  e.  ( R  Cn  S )  /\  ( Rt  k )  e. 
Comp )  ->  ( St  ( F " k ) )  e.  Comp )
3211, 31sylancom 667 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  ( St  ( F
" k ) )  e.  Comp )
33 simplrr 760 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  v  e.  T
)
3420, 23, 25, 30, 32, 33xkoopn 19162 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  { g  e.  ( S  Cn  T
)  |  ( g
" ( F "
k ) )  C_  v }  e.  ( T  ^ko  S ) )
3519, 34eqeltrd 2517 . . . . . . 7  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  { g  e.  ( S  Cn  T
)  |  ( g  o.  F )  e. 
{ h  e.  ( R  Cn  T )  |  ( h "
k )  C_  v } }  e.  ( T  ^ko  S ) )
36 imaeq2 5165 . . . . . . . . 9  |-  ( x  =  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v }  ->  ( `' ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) ) " x
)  =  ( `' ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) ) " {
h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
) )
374mptpreima 5331 . . . . . . . . 9  |-  ( `' ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) ) " {
h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
)  =  { g  e.  ( S  Cn  T )  |  ( g  o.  F )  e.  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } }
3836, 37syl6eq 2491 . . . . . . . 8  |-  ( x  =  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v }  ->  ( `' ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) ) " x
)  =  { g  e.  ( S  Cn  T )  |  ( g  o.  F )  e.  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } } )
3938eleq1d 2509 . . . . . . 7  |-  ( x  =  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v }  ->  ( ( `' ( g  e.  ( S  Cn  T
)  |->  ( g  o.  F ) ) "
x )  e.  ( T  ^ko  S )  <->  { g  e.  ( S  Cn  T
)  |  ( g  o.  F )  e. 
{ h  e.  ( R  Cn  T )  |  ( h "
k )  C_  v } }  e.  ( T  ^ko  S ) ) )
4035, 39syl5ibrcom 222 . . . . . 6  |-  ( ( ( ph  /\  (
k  e.  ~P U. R  /\  v  e.  T
) )  /\  ( Rt  k )  e.  Comp )  ->  ( x  =  { h  e.  ( R  Cn  T )  |  ( h "
k )  C_  v }  ->  ( `' ( g  e.  ( S  Cn  T )  |->  ( g  o.  F ) ) " x )  e.  ( T  ^ko  S ) ) )
4140expimpd 603 . . . . 5  |-  ( (
ph  /\  ( k  e.  ~P U. R  /\  v  e.  T )
)  ->  ( (
( Rt  k )  e. 
Comp  /\  x  =  {
h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
)  ->  ( `' ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) ) " x
)  e.  ( T  ^ko  S ) ) )
4241rexlimdvva 2848 . . . 4  |-  ( ph  ->  ( E. k  e. 
~P  U. R E. v  e.  T  ( ( Rt  k )  e.  Comp  /\  x  =  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } )  ->  ( `' ( g  e.  ( S  Cn  T
)  |->  ( g  o.  F ) ) "
x )  e.  ( T  ^ko  S ) ) )
4310, 42syl5bi 217 . . 3  |-  ( ph  ->  ( x  e.  ran  ( k  e.  {
y  e.  ~P U. R  |  ( Rt  y
)  e.  Comp } , 
v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
)  ->  ( `' ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) ) " x
)  e.  ( T  ^ko  S ) ) )
4443ralrimiv 2798 . 2  |-  ( ph  ->  A. x  e.  ran  ( k  e.  {
y  e.  ~P U. R  |  ( Rt  y
)  e.  Comp } , 
v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
) ( `' ( g  e.  ( S  Cn  T )  |->  ( g  o.  F ) ) " x )  e.  ( T  ^ko  S ) )
45 eqid 2443 . . . . 5  |-  ( T  ^ko  S )  =  ( T  ^ko  S )
4645xkotopon 19173 . . . 4  |-  ( ( S  e.  Top  /\  T  e.  Top )  ->  ( T  ^ko  S )  e.  (TopOn `  ( S  Cn  T
) ) )
4722, 24, 46syl2anc 661 . . 3  |-  ( ph  ->  ( T  ^ko  S )  e.  (TopOn `  ( S  Cn  T
) ) )
48 ovex 6116 . . . . . 6  |-  ( R  Cn  T )  e. 
_V
4948pwex 4475 . . . . 5  |-  ~P ( R  Cn  T )  e. 
_V
506, 7, 8xkotf 19158 . . . . . 6  |-  ( k  e.  { y  e. 
~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h "
k )  C_  v } ) : ( { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp }  X.  T ) --> ~P ( R  Cn  T )
51 frn 5565 . . . . . 6  |-  ( ( k  e.  { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } ) : ( { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp }  X.  T ) --> ~P ( R  Cn  T )  ->  ran  ( k  e.  {
y  e.  ~P U. R  |  ( Rt  y
)  e.  Comp } , 
v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
)  C_  ~P ( R  Cn  T ) )
5250, 51ax-mp 5 . . . . 5  |-  ran  (
k  e.  { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } )  C_  ~P ( R  Cn  T
)
5349, 52ssexi 4437 . . . 4  |-  ran  (
k  e.  { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } )  e.  _V
5453a1i 11 . . 3  |-  ( ph  ->  ran  ( k  e. 
{ y  e.  ~P U. R  |  ( Rt  y )  e.  Comp } , 
v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
)  e.  _V )
55 cntop1 18844 . . . . 5  |-  ( F  e.  ( R  Cn  S )  ->  R  e.  Top )
561, 55syl 16 . . . 4  |-  ( ph  ->  R  e.  Top )
576, 7, 8xkoval 19160 . . . 4  |-  ( ( R  e.  Top  /\  T  e.  Top )  ->  ( T  ^ko  R )  =  (
topGen `  ( fi `  ran  ( k  e.  {
y  e.  ~P U. R  |  ( Rt  y
)  e.  Comp } , 
v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
) ) ) )
5856, 24, 57syl2anc 661 . . 3  |-  ( ph  ->  ( T  ^ko  R )  =  (
topGen `  ( fi `  ran  ( k  e.  {
y  e.  ~P U. R  |  ( Rt  y
)  e.  Comp } , 
v  e.  T  |->  { h  e.  ( R  Cn  T )  |  ( h " k
)  C_  v }
) ) ) )
59 eqid 2443 . . . . 5  |-  ( T  ^ko  R )  =  ( T  ^ko  R )
6059xkotopon 19173 . . . 4  |-  ( ( R  e.  Top  /\  T  e.  Top )  ->  ( T  ^ko  R )  e.  (TopOn `  ( R  Cn  T
) ) )
6156, 24, 60syl2anc 661 . . 3  |-  ( ph  ->  ( T  ^ko  R )  e.  (TopOn `  ( R  Cn  T
) ) )
6247, 54, 58, 61subbascn 18858 . 2  |-  ( ph  ->  ( ( g  e.  ( S  Cn  T
)  |->  ( g  o.  F ) )  e.  ( ( T  ^ko  S )  Cn  ( T  ^ko  R ) )  <->  ( ( g  e.  ( S  Cn  T )  |->  ( g  o.  F ) ) : ( S  Cn  T ) --> ( R  Cn  T )  /\  A. x  e.  ran  (
k  e.  { y  e.  ~P U. R  |  ( Rt  y )  e.  Comp } ,  v  e.  T  |->  { h  e.  ( R  Cn  T
)  |  ( h
" k )  C_  v } ) ( `' ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) ) " x
)  e.  ( T  ^ko  S ) ) ) )
635, 44, 62mpbir2and 913 1  |-  ( ph  ->  ( g  e.  ( S  Cn  T ) 
|->  ( g  o.  F
) )  e.  ( ( T  ^ko  S )  Cn  ( T  ^ko  R ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2715   E.wrex 2716   {crab 2719   _Vcvv 2972    C_ wss 3328   ~Pcpw 3860   U.cuni 4091    e. cmpt 4350    X. cxp 4838   `'ccnv 4839   ran crn 4841   "cima 4843    o. ccom 4844   -->wf 5414   ` cfv 5418  (class class class)co 6091    e. cmpt2 6093   ficfi 7660   ↾t crest 14359   topGenctg 14376   Topctop 18498  TopOnctopon 18499    Cn ccn 18828   Compccmp 18989    ^ko cxko 19134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-iin 4174  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-1st 6577  df-2nd 6578  df-recs 6832  df-rdg 6866  df-1o 6920  df-oadd 6924  df-er 7101  df-map 7216  df-en 7311  df-dom 7312  df-fin 7314  df-fi 7661  df-rest 14361  df-topgen 14382  df-top 18503  df-bases 18505  df-topon 18506  df-cn 18831  df-cmp 18990  df-xko 19136
This theorem is referenced by:  cnmpt1k  19255
  Copyright terms: Public domain W3C validator