Theorem xkoccn 17604

Description: The "constant function" function which maps x e. Y to the constant function z e. X |-> x is a continuous function from X into the space of continuous functions from Y to X. This can also be understood as the currying of the first projection function. (The currying of the second projection function is x e. Y |-> ( z e. X |-> z ), which we already know is continuous because it is a constant function.) (Contributed by Mario Carneiro, 19-Mar-2015.)

Assertion

Ref	Expression
xkoccn	|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( x e. Y |-> ( X X. { x } ) ) e. ( S Cn ( S ^ k o R ) ) )

Distinct variable groups:   x, R   x, S   x, X   x, Y

Proof of Theorem xkoccn

Dummy variables f k v y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnconst2 17301	. . . 4 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) /\ x e. Y ) -> ( X X. { x } ) e. ( R Cn S ) )
2	1	3expa 1153	. . 3 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ x e. Y ) -> ( X X. { x } ) e. ( R Cn S ) )
3		eqid 2404	. . 3 |- ( x e. Y |-> ( X X. { x } ) ) = ( x e. Y |-> ( X X. { x } ) )
4	2, 3	fmptd 5852	. 2 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( x e. Y |-> ( X X. { x } ) ) : Y --> ( R Cn S ) )
5		eqid 2404	. . . . . 6 |- U. R = U. R
6		eqid 2404	. . . . . 6 |- { z e. ~P U. R | ( R ↾t z ) e. Comp } = { z e. ~P U. R | ( R ↾t z ) e. Comp }
7		eqid 2404	. . . . . 6 |- ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) = ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } )
8	5, 6, 7	xkobval 17571	. . . . 5 |- ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) = { y | E. k e. ~P U. R E. v e. S ( ( R ↾t k ) e. Comp /\ y = { f e. ( R Cn S ) | ( f " k ) C_ v } ) }
9	8	abeq2i 2511	. . . 4 |- ( y e. ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) <-> E. k e. ~P U. R E. v e. S ( ( R ↾t k ) e. Comp /\ y = { f e. ( R Cn S ) | ( f " k ) C_ v } ) )
10	2	adantlr 696	. . . . . . . . . . . . . 14 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ x e. Y ) -> ( X X. { x } ) e. ( R Cn S ) )
11	10	adantlr 696	. . . . . . . . . . . . 13 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ x e. Y ) -> ( X X. { x } ) e. ( R Cn S ) )
12	11	adantlr 696	. . . . . . . . . . . 12 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) /\ x e. Y ) -> ( X X. { x } ) e. ( R Cn S ) )
13		simplr 732	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) /\ x e. Y ) -> k = (/) )
14	13	imaeq2d 5162	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) /\ x e. Y ) -> ( ( X X. { x } ) " k ) = ( ( X X. { x } ) " (/) ) )
15		ima0 5180	. . . . . . . . . . . . . 14 |- ( ( X X. { x } ) " (/) ) = (/)
16		0ss 3616	. . . . . . . . . . . . . 14 |- (/) C_ v
17	15, 16	eqsstri 3338	. . . . . . . . . . . . 13 |- ( ( X X. { x } ) " (/) ) C_ v
18	14, 17	syl6eqss 3358	. . . . . . . . . . . 12 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) /\ x e. Y ) -> ( ( X X. { x } ) " k ) C_ v )
19		imaeq1 5157	. . . . . . . . . . . . . 14 |- ( f = ( X X. { x } ) -> ( f " k ) = ( ( X X. { x } ) " k ) )
20	19	sseq1d 3335	. . . . . . . . . . . . 13 |- ( f = ( X X. { x } ) -> ( ( f " k ) C_ v <-> ( ( X X. { x } ) " k ) C_ v ) )
21	20	elrab 3052	. . . . . . . . . . . 12 |- ( ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } <-> ( ( X X. { x } ) e. ( R Cn S ) /\ ( ( X X. { x } ) " k ) C_ v ) )
22	12, 18, 21	sylanbrc 646	. . . . . . . . . . 11 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) /\ x e. Y ) -> ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } )
23	22	ralrimiva 2749	. . . . . . . . . 10 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) -> A. x e. Y ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } )
24		rabid2 2845	. . . . . . . . . 10 |- ( Y = { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } <-> A. x e. Y ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } )
25	23, 24	sylibr 204	. . . . . . . . 9 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) -> Y = { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } )
26		simpllr 736	. . . . . . . . . . 11 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) -> S e. (TopOn ` Y ) )
27		toponmax 16948	. . . . . . . . . . 11 |- ( S e. (TopOn ` Y ) -> Y e. S )
28	26, 27	syl 16	. . . . . . . . . 10 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) -> Y e. S )
29	28	adantr 452	. . . . . . . . 9 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) -> Y e. S )
30	25, 29	eqeltrrd 2479	. . . . . . . 8 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k = (/) ) -> { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } e. S )
31		ifnefalse 3707	. . . . . . . . . . . . . . 15 |- ( k =/= (/) -> if ( k = (/) , Y , v ) = v )
32	31	ad2antlr 708	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> if ( k = (/) , Y , v ) = v )
33	32	eleq2d 2471	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( x e. if ( k = (/) , Y , v ) <-> x e. v ) )
34		vex 2919	. . . . . . . . . . . . . . . 16 |- x e. _V
35	34	snss 3886	. . . . . . . . . . . . . . 15 |- ( x e. v <-> { x } C_ v )
36	33, 35	syl6bb 253	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( x e. if ( k = (/) , Y , v ) <-> { x } C_ v ) )
37		df-ima 4850	. . . . . . . . . . . . . . . . 17 |- ( ( X X. { x } ) " k ) = ran ( ( X X. { x } ) |` k )
38		simplrl 737	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) -> k e. ~P U. R )
39	38	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> k e. ~P U. R )
40	39	elpwid 3768	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> k C_ U. R )
41		toponuni 16947	. . . . . . . . . . . . . . . . . . . . 21 |- ( R e. (TopOn ` X ) -> X = U. R )
42	41	ad5antr 715	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> X = U. R )
43	40, 42	sseqtr4d 3345	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> k C_ X )
44		xpssres 5139	. . . . . . . . . . . . . . . . . . 19 |- ( k C_ X -> ( ( X X. { x } ) |` k ) = ( k X. { x } ) )
45	43, 44	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( ( X X. { x } ) |` k ) = ( k X. { x } ) )
46	45	rneqd 5056	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ran ( ( X X. { x } ) |` k ) = ran ( k X. { x } ) )
47	37, 46	syl5eq 2448	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( ( X X. { x } ) " k ) = ran ( k X. { x } ) )
48		rnxp 5258	. . . . . . . . . . . . . . . . 17 |- ( k =/= (/) -> ran ( k X. { x } ) = { x } )
49	48	ad2antlr 708	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ran ( k X. { x } ) = { x } )
50	47, 49	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( ( X X. { x } ) " k ) = { x } )
51	50	sseq1d 3335	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( ( ( X X. { x } ) " k ) C_ v <-> { x } C_ v ) )
52	11	adantlr 696	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( X X. { x } ) e. ( R Cn S ) )
53	52	biantrurd 495	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( ( ( X X. { x } ) " k ) C_ v <-> ( ( X X. { x } ) e. ( R Cn S ) /\ ( ( X X. { x } ) " k ) C_ v ) ) )
54	36, 51, 53	3bitr2d 273	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( x e. if ( k = (/) , Y , v ) <-> ( ( X X. { x } ) e. ( R Cn S ) /\ ( ( X X. { x } ) " k ) C_ v ) ) )
55	33, 54	bitr3d 247	. . . . . . . . . . . 12 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( x e. v <-> ( ( X X. { x } ) e. ( R Cn S ) /\ ( ( X X. { x } ) " k ) C_ v ) ) )
56	55, 21	syl6bbr 255	. . . . . . . . . . 11 |- ( ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) /\ x e. Y ) -> ( x e. v <-> ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } ) )
57	56	rabbi2dva 3509	. . . . . . . . . 10 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) -> ( Y i^i v ) = { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } )
58		simplrr 738	. . . . . . . . . . . . 13 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) -> v e. S )
59		toponss 16949	. . . . . . . . . . . . 13 |- ( ( S e. (TopOn ` Y ) /\ v e. S ) -> v C_ Y )
60	26, 58, 59	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) -> v C_ Y )
61	60	adantr 452	. . . . . . . . . . 11 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) -> v C_ Y )
62		dfss1 3505	. . . . . . . . . . 11 |- ( v C_ Y <-> ( Y i^i v ) = v )
63	61, 62	sylib 189	. . . . . . . . . 10 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) -> ( Y i^i v ) = v )
64	57, 63	eqtr3d 2438	. . . . . . . . 9 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) -> { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } = v )
65	58	adantr 452	. . . . . . . . 9 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) -> v e. S )
66	64, 65	eqeltrd 2478	. . . . . . . 8 |- ( ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) /\ k =/= (/) ) -> { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } e. S )
67	30, 66	pm2.61dane 2645	. . . . . . 7 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) -> { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } e. S )
68		imaeq2 5158	. . . . . . . . 9 |- ( y = { f e. ( R Cn S ) | ( f " k ) C_ v } -> ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) = ( `' ( x e. Y |-> ( X X. { x } ) ) " { f e. ( R Cn S ) | ( f " k ) C_ v } ) )
69	3	mptpreima 5322	. . . . . . . . 9 |- ( `' ( x e. Y |-> ( X X. { x } ) ) " { f e. ( R Cn S ) | ( f " k ) C_ v } ) = { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } }
70	68, 69	syl6eq 2452	. . . . . . . 8 |- ( y = { f e. ( R Cn S ) | ( f " k ) C_ v } -> ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) = { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } )
71	70	eleq1d 2470	. . . . . . 7 |- ( y = { f e. ( R Cn S ) | ( f " k ) C_ v } -> ( ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) e. S <-> { x e. Y | ( X X. { x } ) e. { f e. ( R Cn S ) | ( f " k ) C_ v } } e. S ) )
72	67, 71	syl5ibrcom 214	. . . . . 6 |- ( ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R ↾t k ) e. Comp ) -> ( y = { f e. ( R Cn S ) | ( f " k ) C_ v } -> ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) e. S ) )
73	72	expimpd 587	. . . . 5 |- ( ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) -> ( ( ( R ↾t k ) e. Comp /\ y = { f e. ( R Cn S ) | ( f " k ) C_ v } ) -> ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) e. S ) )
74	73	rexlimdvva 2797	. . . 4 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( E. k e. ~P U. R E. v e. S ( ( R ↾t k ) e. Comp /\ y = { f e. ( R Cn S ) | ( f " k ) C_ v } ) -> ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) e. S ) )
75	9, 74	syl5bi 209	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( y e. ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) -> ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) e. S ) )
76	75	ralrimiv 2748	. 2 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> A. y e. ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) e. S )
77		simpr 448	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> S e. (TopOn ` Y ) )
78		ovex 6065	. . . . . 6 |- ( R Cn S ) e. _V
79	78	pwex 4342	. . . . 5 |- ~P ( R Cn S ) e. _V
80	5, 6, 7	xkotf 17570	. . . . . 6 |- ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) : ( { z e. ~P U. R | ( R ↾t z ) e. Comp } X. S ) --> ~P ( R Cn S )
81		frn 5556	. . . . . 6 |- ( ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) : ( { z e. ~P U. R | ( R ↾t z ) e. Comp } X. S ) --> ~P ( R Cn S ) -> ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) C_ ~P ( R Cn S ) )
82	80, 81	ax-mp 8	. . . . 5 |- ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) C_ ~P ( R Cn S )
83	79, 82	ssexi 4308	. . . 4 |- ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) e. _V
84	83	a1i 11	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) e. _V )
85		topontop 16946	. . . 4 |- ( R e. (TopOn ` X ) -> R e. Top )
86		topontop 16946	. . . 4 |- ( S e. (TopOn ` Y ) -> S e. Top )
87	5, 6, 7	xkoval 17572	. . . 4 |- ( ( R e. Top /\ S e. Top ) -> ( S ^ k o R ) = ( topGen ` ( fi ` ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ) ) )
88	85, 86, 87	syl2an 464	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( S ^ k o R ) = ( topGen ` ( fi ` ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ) ) )
89		eqid 2404	. . . . 5 |- ( S ^ k o R ) = ( S ^ k o R )
90	89	xkotopon 17585	. . . 4 |- ( ( R e. Top /\ S e. Top ) -> ( S ^ k o R ) e. (TopOn ` ( R Cn S ) ) )
91	85, 86, 90	syl2an 464	. . 3 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( S ^ k o R ) e. (TopOn ` ( R Cn S ) ) )
92	77, 84, 88, 91	subbascn 17272	. 2 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( ( x e. Y |-> ( X X. { x } ) ) e. ( S Cn ( S ^ k o R ) ) <-> ( ( x e. Y |-> ( X X. { x } ) ) : Y --> ( R Cn S ) /\ A. y e. ran ( k e. { z e. ~P U. R | ( R ↾t z ) e. Comp } , v e. S |-> { f e. ( R Cn S ) | ( f " k ) C_ v } ) ( `' ( x e. Y |-> ( X X. { x } ) ) " y ) e. S ) ) )
93	4, 76, 92	mpbir2and 889	1 |- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( x e. Y |-> ( X X. { x } ) ) e. ( S Cn ( S ^ k o R ) ) )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   {crab 2670   _Vcvv 2916   i^i cin 3279   C_ wss 3280   (/)c0 3588   ifcif 3699   ~Pcpw 3759   {csn 3774   U.cuni 3975   e. cmpt 4226   X. cxp 4835   `'ccnv 4836   ran crn 4838   |` cres 4839   "cima 4840   -->wf 5409   ` cfv 5413  (class class class)co 6040   e. cmpt2 6042   ficfi 7373   ↾_t crest 13603   topGenctg 13620   Topctop 16913  TopOnctopon 16914   Cn ccn 17242   Compccmp 17403   ^ k o cxko 17546

This theorem is referenced by:  cnmptkc  17664  xkofvcn  17669

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-fin 7072  df-fi 7374  df-rest 13605  df-topgen 13622  df-top 16918  df-bases 16920  df-topon 16921  df-cn 17245  df-cnp 17246  df-cmp 17404  df-xko 17548