Metamath Proof Explorer

Theorem xkoccn

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)

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

Proof

Step Hyp Ref Expression
1 cnconst2 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) /\ x e. Y ) -> ( X X. { x } ) e. ( R Cn S ) )
2 1 3expa 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ x e. Y ) -> ( X X. { x } ) e. ( R Cn S ) )
3 2 fmpttd 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( x e. Y |-> ( X X. { x } ) ) : Y --> ( R Cn S ) )
4 eqid 
 |-  U. R = U. R
5 eqid 
 |-  { z e. ~P U. R | ( R |`t z ) e. Comp } = { z e. ~P U. R | ( R |`t z ) e. Comp }
6 eqid 
 |-  ( 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 } )
7 4 5 6 xkobval 
 |-  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 } ) }
8 7 abeq2i 
 |-  ( 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 } ) )
9 2 ad5ant15 
 |-  ( ( ( ( ( ( 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 ) )
10 simplr 
 |-  ( ( ( ( ( ( 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 = (/) )
11 10 imaeq2d 
 |-  ( ( ( ( ( ( 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 } ) " (/) ) )
12 ima0 
 |-  ( ( X X. { x } ) " (/) ) = (/)
13 0ss 
 |-  (/) C_ v
14 12 13 eqsstri 
 |-  ( ( X X. { x } ) " (/) ) C_ v
15 11 14 eqsstrdi 
 |-  ( ( ( ( ( ( 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 )
16 imaeq1 
 |-  ( f = ( X X. { x } ) -> ( f " k ) = ( ( X X. { x } ) " k ) )
17 16 sseq1d 
 |-  ( f = ( X X. { x } ) -> ( ( f " k ) C_ v <-> ( ( X X. { x } ) " k ) C_ v ) )
18 17 elrab 
 |-  ( ( 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 ) )
19 9 15 18 sylanbrc 
 |-  ( ( ( ( ( ( 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 } )
20 19 ralrimiva 
 |-  ( ( ( ( ( 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 } )
21 rabid2 
 |-  ( 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 } )
22 20 21 sylibr 
 |-  ( ( ( ( ( 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 } } )
23 simpllr 
 |-  ( ( ( ( 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 ) )
24 toponmax 
 |-  ( S e. ( TopOn ` Y ) -> Y e. S )
25 23 24 syl 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R |`t k ) e. Comp ) -> Y e. S )
26 25 adantr 
 |-  ( ( ( ( ( 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 )
27 22 26 eqeltrrd 
 |-  ( ( ( ( ( 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 )
28 ifnefalse 
 |-  ( k =/= (/) -> if ( k = (/) , Y , v ) = v )
29 28 ad2antlr 
 |-  ( ( ( ( ( ( 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 )
30 29 eleq2d 
 |-  ( ( ( ( ( ( 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 ) )
31 vex 
 |-  x e. _V
32 31 snss 
 |-  ( x e. v <-> { x } C_ v )
33 30 32 bitrdi 
 |-  ( ( ( ( ( ( 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 ) )
34 df-ima 
 |-  ( ( X X. { x } ) " k ) = ran ( ( X X. { x } ) |` k )
35 simplrl 
 |-  ( ( ( ( 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 )
36 35 ad2antrr 
 |-  ( ( ( ( ( ( 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 )
37 36 elpwid 
 |-  ( ( ( ( ( ( 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 )
38 toponuni 
 |-  ( R e. ( TopOn ` X ) -> X = U. R )
39 38 ad5antr 
 |-  ( ( ( ( ( ( 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 )
40 37 39 sseqtrrd 
 |-  ( ( ( ( ( ( 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 )
41 xpssres 
 |-  ( k C_ X -> ( ( X X. { x } ) |` k ) = ( k X. { x } ) )
42 40 41 syl 
 |-  ( ( ( ( ( ( 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 } ) )
43 42 rneqd 
 |-  ( ( ( ( ( ( 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 } ) )
44 34 43 syl5eq 
 |-  ( ( ( ( ( ( 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 } ) )
45 rnxp 
 |-  ( k =/= (/) -> ran ( k X. { x } ) = { x } )
46 45 ad2antlr 
 |-  ( ( ( ( ( ( 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 } )
47 44 46 eqtrd 
 |-  ( ( ( ( ( ( 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 } )
48 47 sseq1d 
 |-  ( ( ( ( ( ( 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 ) )
49 2 ad5ant15 
 |-  ( ( ( ( ( ( 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 ) )
50 49 biantrurd 
 |-  ( ( ( ( ( ( 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 ) ) )
51 33 48 50 3bitr2d 
 |-  ( ( ( ( ( ( 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 ) ) )
52 30 51 bitr3d 
 |-  ( ( ( ( ( ( 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 ) ) )
53 52 18 bitr4di 
 |-  ( ( ( ( ( ( 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 } ) )
54 53 rabbi2dva 
 |-  ( ( ( ( ( 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 } } )
55 simplrr 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R |`t k ) e. Comp ) -> v e. S )
56 toponss 
 |-  ( ( S e. ( TopOn ` Y ) /\ v e. S ) -> v C_ Y )
57 23 55 56 syl2anc 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. R /\ v e. S ) ) /\ ( R |`t k ) e. Comp ) -> v C_ Y )
58 57 adantr 
 |-  ( ( ( ( ( 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 )
59 sseqin2 
 |-  ( v C_ Y <-> ( Y i^i v ) = v )
60 58 59 sylib 
 |-  ( ( ( ( ( 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 )
61 54 60 eqtr3d 
 |-  ( ( ( ( ( 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 )
62 55 adantr 
 |-  ( ( ( ( ( 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 )
63 61 62 eqeltrd 
 |-  ( ( ( ( ( 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 )
64 27 63 pm2.61dane 
 |-  ( ( ( ( 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 )
65 imaeq2 
 |-  ( 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 } ) )
66 eqid 
 |-  ( x e. Y |-> ( X X. { x } ) ) = ( x e. Y |-> ( X X. { x } ) )
67 66 mptpreima 
 |-  ( `' ( 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 } }
68 65 67 eqtrdi 
 |-  ( 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 } } )
69 68 eleq1d 
 |-  ( 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 ) )
70 64 69 syl5ibrcom 
 |-  ( ( ( ( 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 ) )
71 70 expimpd 
 |-  ( ( ( 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 ) )
72 71 rexlimdvva 
 |-  ( ( 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 ) )
73 8 72 syl5bi 
 |-  ( ( 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 ) )
74 73 ralrimiv 
 |-  ( ( 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 )
75 simpr 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> S e. ( TopOn ` Y ) )
76 ovex 
 |-  ( R Cn S ) e. _V
77 76 pwex 
 |-  ~P ( R Cn S ) e. _V
78 4 5 6 xkotf 
 |-  ( 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 )
79 frn 
 |-  ( ( 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 ) )
80 78 79 ax-mp 
 |-  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 )
81 77 80 ssexi 
 |-  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
82 81 a1i 
 |-  ( ( 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 )
83 topontop 
 |-  ( R e. ( TopOn ` X ) -> R e. Top )
84 topontop 
 |-  ( S e. ( TopOn ` Y ) -> S e. Top )
85 4 5 6 xkoval 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko 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 } ) ) ) )
86 83 84 85 syl2an 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( S ^ko 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 } ) ) ) )
87 eqid 
 |-  ( S ^ko R ) = ( S ^ko R )
88 87 xkotopon 
 |-  ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
89 83 84 88 syl2an 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) )
90 75 82 86 89 subbascn 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( ( x e. Y |-> ( X X. { x } ) ) e. ( S Cn ( S ^ko 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 ) ) )
91 3 74 90 mpbir2and 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( x e. Y |-> ( X X. { x } ) ) e. ( S Cn ( S ^ko R ) ) )