Theorem xkoco2cn 21461

Description: If F is a continuous function, then g |-> F o. g is a continuous function on function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.)

Hypotheses

Ref	Expression
xkoco2cn.r	|- ( ph -> R e. Top )
xkoco2cn.f	|- ( ph -> F e. ( S Cn T ) )

Assertion

Ref	Expression
xkoco2cn	|- ( ph -> ( g e. ( R Cn S ) |-> ( F o. g ) ) e. ( ( S ^ko R ) Cn ( T ^ko R ) ) )

Distinct variable groups:   ph, g   R, g   S, g   T, g   g, F

Proof of Theorem xkoco2cn

Dummy variables k v x h y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 477	. . . 4 |- ( ( ph /\ g e. ( R Cn S ) ) -> g e. ( R Cn S ) )
2		xkoco2cn.f	. . . . 5 |- ( ph -> F e. ( S Cn T ) )
3	2	adantr 481	. . . 4 |- ( ( ph /\ g e. ( R Cn S ) ) -> F e. ( S Cn T ) )
4		cnco 21070	. . . 4 |- ( ( g e. ( R Cn S ) /\ F e. ( S Cn T ) ) -> ( F o. g ) e. ( R Cn T ) )
5	1, 3, 4	syl2anc 693	. . 3 |- ( ( ph /\ g e. ( R Cn S ) ) -> ( F o. g ) e. ( R Cn T ) )
6		eqid 2622	. . 3 |- ( g e. ( R Cn S ) |-> ( F o. g ) ) = ( g e. ( R Cn S ) |-> ( F o. g ) )
7	5, 6	fmptd 6385	. 2 |- ( ph -> ( g e. ( R Cn S ) |-> ( F o. g ) ) : ( R Cn S ) --> ( R Cn T ) )
8		eqid 2622	. . . . . 6 |- U. R = U. R
9		eqid 2622	. . . . . 6 |- { y e. ~P U. R | ( R ↾t y ) e. Comp } = { y e. ~P U. R | ( R ↾t y ) e. Comp }
10		eqid 2622	. . . . . 6 |- ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) = ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } )
11	8, 9, 10	xkobval 21389	. . . . 5 |- ran ( k e. { y e. ~P U. R | ( R ↾t 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 ( ( R ↾t k ) e. Comp /\ x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) }
12	11	abeq2i 2735	. . . 4 |- ( x e. ran ( k e. { y e. ~P U. R | ( R ↾t 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 ( ( R ↾t k ) e. Comp /\ x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
13		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> g e. ( R Cn S ) )
14	2	ad3antrrr 766	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> F e. ( S Cn T ) )
15	13, 14, 4	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( F o. g ) e. ( R Cn T ) )
16		imaeq1 5461	. . . . . . . . . . . . . 14 |- ( h = ( F o. g ) -> ( h " k ) = ( ( F o. g ) " k ) )
17		imaco 5640	. . . . . . . . . . . . . 14 |- ( ( F o. g ) " k ) = ( F " ( g " k ) )
18	16, 17	syl6eq 2672	. . . . . . . . . . . . 13 |- ( h = ( F o. g ) -> ( h " k ) = ( F " ( g " k ) ) )
19	18	sseq1d 3632	. . . . . . . . . . . 12 |- ( h = ( F o. g ) -> ( ( h " k ) C_ v <-> ( F " ( g " k ) ) C_ v ) )
20	19	elrab3 3364	. . . . . . . . . . 11 |- ( ( F o. g ) e. ( R Cn T ) -> ( ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( F " ( g " k ) ) C_ v ) )
21	15, 20	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( F " ( g " k ) ) C_ v ) )
22		eqid 2622	. . . . . . . . . . . . . . 15 |- U. S = U. S
23		eqid 2622	. . . . . . . . . . . . . . 15 |- U. T = U. T
24	22, 23	cnf 21050	. . . . . . . . . . . . . 14 |- ( F e. ( S Cn T ) -> F : U. S --> U. T )
25	2, 24	syl 17	. . . . . . . . . . . . 13 |- ( ph -> F : U. S --> U. T )
26	25	ad3antrrr 766	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> F : U. S --> U. T )
27		ffun 6048	. . . . . . . . . . . 12 |- ( F : U. S --> U. T -> Fun F )
28	26, 27	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> Fun F )
29		imassrn 5477	. . . . . . . . . . . . 13 |- ( g " k ) C_ ran g
30	8, 22	cnf 21050	. . . . . . . . . . . . . . 15 |- ( g e. ( R Cn S ) -> g : U. R --> U. S )
31	13, 30	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> g : U. R --> U. S )
32		frn 6053	. . . . . . . . . . . . . 14 |- ( g : U. R --> U. S -> ran g C_ U. S )
33	31, 32	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ran g C_ U. S )
34	29, 33	syl5ss 3614	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( g " k ) C_ U. S )
35		fdm 6051	. . . . . . . . . . . . 13 |- ( F : U. S --> U. T -> dom F = U. S )
36	26, 35	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> dom F = U. S )
37	34, 36	sseqtr4d 3642	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( g " k ) C_ dom F )
38		funimass3 6333	. . . . . . . . . . 11 |- ( ( Fun F /\ ( g " k ) C_ dom F ) -> ( ( F " ( g " k ) ) C_ v <-> ( g " k ) C_ ( `' F " v ) ) )
39	28, 37, 38	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( ( F " ( g " k ) ) C_ v <-> ( g " k ) C_ ( `' F " v ) ) )
40	21, 39	bitrd 268	. . . . . . . . 9 |- ( ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) /\ g e. ( R Cn S ) ) -> ( ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( g " k ) C_ ( `' F " v ) ) )
41	40	rabbidva 3188	. . . . . . . 8 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } = { g e. ( R Cn S ) | ( g " k ) C_ ( `' F " v ) } )
42		xkoco2cn.r	. . . . . . . . . 10 |- ( ph -> R e. Top )
43	42	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> R e. Top )
44		cntop1 21044	. . . . . . . . . . 11 |- ( F e. ( S Cn T ) -> S e. Top )
45	2, 44	syl 17	. . . . . . . . . 10 |- ( ph -> S e. Top )
46	45	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> S e. Top )
47		simplrl 800	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> k e. ~P U. R )
48	47	elpwid 4170	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> k C_ U. R )
49		simpr 477	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> ( R ↾t k ) e. Comp )
50	2	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> F e. ( S Cn T ) )
51		simplrr 801	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> v e. T )
52		cnima 21069	. . . . . . . . . 10 |- ( ( F e. ( S Cn T ) /\ v e. T ) -> ( `' F " v ) e. S )
53	50, 51, 52	syl2anc 693	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> ( `' F " v ) e. S )
54	8, 43, 46, 48, 49, 53	xkoopn 21392	. . . . . . . 8 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> { g e. ( R Cn S ) | ( g " k ) C_ ( `' F " v ) } e. ( S ^ko R ) )
55	41, 54	eqeltrd 2701	. . . . . . 7 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } e. ( S ^ko R ) )
56		imaeq2 5462	. . . . . . . . 9 |- ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) = ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " { h e. ( R Cn T ) | ( h " k ) C_ v } ) )
57	6	mptpreima 5628	. . . . . . . . 9 |- ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " { h e. ( R Cn T ) | ( h " k ) C_ v } ) = { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } }
58	56, 57	syl6eq 2672	. . . . . . . 8 |- ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) = { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } )
59	58	eleq1d 2686	. . . . . . 7 |- ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) <-> { g e. ( R Cn S ) | ( F o. g ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } } e. ( S ^ko R ) ) )
60	55, 59	syl5ibrcom 237	. . . . . 6 |- ( ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) /\ ( R ↾t k ) e. Comp ) -> ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) )
61	60	expimpd 629	. . . . 5 |- ( ( ph /\ ( k e. ~P U. R /\ v e. T ) ) -> ( ( ( R ↾t k ) e. Comp /\ x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) )
62	61	rexlimdvva 3038	. . . 4 |- ( ph -> ( E. k e. ~P U. R E. v e. T ( ( R ↾t k ) e. Comp /\ x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) )
63	12, 62	syl5bi 232	. . 3 |- ( ph -> ( x e. ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) )
64	63	ralrimiv 2965	. 2 |- ( ph -> A. x e. ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) )
65		eqid 2622	. . . . 5 |- ( S ^ko R ) = ( S ^ko R )
66	65	xkotopon 21403	. . . 4 |- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. (TopOn ` ( R Cn S ) ) )
67	42, 45, 66	syl2anc 693	. . 3 |- ( ph -> ( S ^ko R ) e. (TopOn ` ( R Cn S ) ) )
68		ovex 6678	. . . . . 6 |- ( R Cn T ) e. _V
69	68	pwex 4848	. . . . 5 |- ~P ( R Cn T ) e. _V
70	8, 9, 10	xkotf 21388	. . . . . 6 |- ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) : ( { y e. ~P U. R | ( R ↾t y ) e. Comp } X. T ) --> ~P ( R Cn T )
71		frn 6053	. . . . . 6 |- ( ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) : ( { y e. ~P U. R | ( R ↾t y ) e. Comp } X. T ) --> ~P ( R Cn T ) -> ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) C_ ~P ( R Cn T ) )
72	70, 71	ax-mp 5	. . . . 5 |- ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) C_ ~P ( R Cn T )
73	69, 72	ssexi 4803	. . . 4 |- ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. _V
74	73	a1i 11	. . 3 |- ( ph -> ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. _V )
75		cntop2 21045	. . . . 5 |- ( F e. ( S Cn T ) -> T e. Top )
76	2, 75	syl 17	. . . 4 |- ( ph -> T e. Top )
77	8, 9, 10	xkoval 21390	. . . 4 |- ( ( R e. Top /\ T e. Top ) -> ( T ^ko R ) = ( topGen ` ( fi ` ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
78	42, 76, 77	syl2anc 693	. . 3 |- ( ph -> ( T ^ko R ) = ( topGen ` ( fi ` ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) )
79		eqid 2622	. . . . 5 |- ( T ^ko R ) = ( T ^ko R )
80	79	xkotopon 21403	. . . 4 |- ( ( R e. Top /\ T e. Top ) -> ( T ^ko R ) e. (TopOn ` ( R Cn T ) ) )
81	42, 76, 80	syl2anc 693	. . 3 |- ( ph -> ( T ^ko R ) e. (TopOn ` ( R Cn T ) ) )
82	67, 74, 78, 81	subbascn 21058	. 2 |- ( ph -> ( ( g e. ( R Cn S ) |-> ( F o. g ) ) e. ( ( S ^ko R ) Cn ( T ^ko R ) ) <-> ( ( g e. ( R Cn S ) |-> ( F o. g ) ) : ( R Cn S ) --> ( R Cn T ) /\ A. x e. ran ( k e. { y e. ~P U. R | ( R ↾t y ) e. Comp } , v e. T |-> { h e. ( R Cn T ) | ( h " k ) C_ v } ) ( `' ( g e. ( R Cn S ) |-> ( F o. g ) ) " x ) e. ( S ^ko R ) ) ) )
83	7, 64, 82	mpbir2and 957	1 |- ( ph -> ( g e. ( R Cn S ) |-> ( F o. g ) ) e. ( ( S ^ko R ) Cn ( T ^ko R ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   C_ wss 3574   ~Pcpw 4158   U.cuni 4436   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   o. ccom 5118   Fun wfun 5882   -->wf 5884   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   ficfi 8316   ↾_t crest 16081   topGenctg 16098   Topctop 20698  TopOnctopon 20715   Cn ccn 21028   Compccmp 21189   ^ko cxko 21364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cn 21031  df-cmp 21190  df-xko 21366

This theorem is referenced by:  cnmptk1  21484