Metamath Proof Explorer

Theorem xkoinjcn

Description: Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis xkoinjcn.3 
|- F = ( x e. X |-> ( y e. Y |-> <. y , x >. ) )
Assertion xkoinjcn 
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> F e. ( R Cn ( ( S tX R ) ^ko S ) ) )

Proof

Step Hyp Ref Expression
1 xkoinjcn.3 
 |-  F = ( x e. X |-> ( y e. Y |-> <. y , x >. ) )
2 simplr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ x e. X ) -> S e. ( TopOn ` Y ) )
3 2 cnmptid 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ x e. X ) -> ( y e. Y |-> y ) e. ( S Cn S ) )
4 simpll 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ x e. X ) -> R e. ( TopOn ` X ) )
5 simpr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ x e. X ) -> x e. X )
6 2 4 5 cnmptc 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ x e. X ) -> ( y e. Y |-> x ) e. ( S Cn R ) )
7 2 3 6 cnmpt1t 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ x e. X ) -> ( y e. Y |-> <. y , x >. ) e. ( S Cn ( S tX R ) ) )
8 7 1 fmptd 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> F : X --> ( S Cn ( S tX R ) ) )
9 eqid 
 |-  U. S = U. S
10 eqid 
 |-  { w e. ~P U. S | ( S |`t w ) e. Comp } = { w e. ~P U. S | ( S |`t w ) e. Comp }
11 eqid 
 |-  ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) = ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } )
12 9 10 11 xkobval 
 |-  ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) = { z | E. k e. ~P U. S E. v e. ( S tX R ) ( ( S |`t k ) e. Comp /\ z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) }
13 12 abeq2i 
 |-  ( z e. ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) <-> E. k e. ~P U. S E. v e. ( S tX R ) ( ( S |`t k ) e. Comp /\ z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) )
14 simpll 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) )
15 14 7 sylan 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) -> ( y e. Y |-> <. y , x >. ) e. ( S Cn ( S tX R ) ) )
16 imaeq1 
 |-  ( f = ( y e. Y |-> <. y , x >. ) -> ( f " k ) = ( ( y e. Y |-> <. y , x >. ) " k ) )
17 16 sseq1d 
 |-  ( f = ( y e. Y |-> <. y , x >. ) -> ( ( f " k ) C_ v <-> ( ( y e. Y |-> <. y , x >. ) " k ) C_ v ) )
18 17 elrab3 
 |-  ( ( y e. Y |-> <. y , x >. ) e. ( S Cn ( S tX R ) ) -> ( ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } <-> ( ( y e. Y |-> <. y , x >. ) " k ) C_ v ) )
19 15 18 syl 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) -> ( ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } <-> ( ( y e. Y |-> <. y , x >. ) " k ) C_ v ) )
20 funmpt 
 |-  Fun ( y e. Y |-> <. y , x >. )
21 simplrl 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> k e. ~P U. S )
22 21 elpwid 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> k C_ U. S )
23 14 simprd 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> S e. ( TopOn ` Y ) )
24 toponuni 
 |-  ( S e. ( TopOn ` Y ) -> Y = U. S )
25 23 24 syl 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> Y = U. S )
26 22 25 sseqtrrd 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> k C_ Y )
27 26 adantr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) -> k C_ Y )
28 dmmptg 
 |-  ( A. y e. Y <. y , x >. e. _V -> dom ( y e. Y |-> <. y , x >. ) = Y )
29 opex 
 |-  <. y , x >. e. _V
30 29 a1i 
 |-  ( y e. Y -> <. y , x >. e. _V )
31 28 30 mprg 
 |-  dom ( y e. Y |-> <. y , x >. ) = Y
32 27 31 sseqtrrdi 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) -> k C_ dom ( y e. Y |-> <. y , x >. ) )
33 funimass4 
 |-  ( ( Fun ( y e. Y |-> <. y , x >. ) /\ k C_ dom ( y e. Y |-> <. y , x >. ) ) -> ( ( ( y e. Y |-> <. y , x >. ) " k ) C_ v <-> A. z e. k ( ( y e. Y |-> <. y , x >. ) ` z ) e. v ) )
34 20 32 33 sylancr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) -> ( ( ( y e. Y |-> <. y , x >. ) " k ) C_ v <-> A. z e. k ( ( y e. Y |-> <. y , x >. ) ` z ) e. v ) )
35 27 sselda 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) /\ z e. k ) -> z e. Y )
36 opeq1 
 |-  ( y = z -> <. y , x >. = <. z , x >. )
37 eqid 
 |-  ( y e. Y |-> <. y , x >. ) = ( y e. Y |-> <. y , x >. )
38 opex 
 |-  <. z , x >. e. _V
39 36 37 38 fvmpt 
 |-  ( z e. Y -> ( ( y e. Y |-> <. y , x >. ) ` z ) = <. z , x >. )
40 35 39 syl 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) /\ z e. k ) -> ( ( y e. Y |-> <. y , x >. ) ` z ) = <. z , x >. )
41 40 eleq1d 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) /\ z e. k ) -> ( ( ( y e. Y |-> <. y , x >. ) ` z ) e. v <-> <. z , x >. e. v ) )
42 vex 
 |-  x e. _V
43 opeq2 
 |-  ( w = x -> <. z , w >. = <. z , x >. )
44 43 eleq1d 
 |-  ( w = x -> ( <. z , w >. e. v <-> <. z , x >. e. v ) )
45 42 44 ralsn 
 |-  ( A. w e. { x } <. z , w >. e. v <-> <. z , x >. e. v )
46 41 45 bitr4di 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) /\ z e. k ) -> ( ( ( y e. Y |-> <. y , x >. ) ` z ) e. v <-> A. w e. { x } <. z , w >. e. v ) )
47 46 ralbidva 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) -> ( A. z e. k ( ( y e. Y |-> <. y , x >. ) ` z ) e. v <-> A. z e. k A. w e. { x } <. z , w >. e. v ) )
48 dfss3 
 |-  ( ( k X. { x } ) C_ v <-> A. t e. ( k X. { x } ) t e. v )
49 eleq1 
 |-  ( t = <. z , w >. -> ( t e. v <-> <. z , w >. e. v ) )
50 49 ralxp 
 |-  ( A. t e. ( k X. { x } ) t e. v <-> A. z e. k A. w e. { x } <. z , w >. e. v )
51 48 50 bitri 
 |-  ( ( k X. { x } ) C_ v <-> A. z e. k A. w e. { x } <. z , w >. e. v )
52 47 51 bitr4di 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) -> ( A. z e. k ( ( y e. Y |-> <. y , x >. ) ` z ) e. v <-> ( k X. { x } ) C_ v ) )
53 19 34 52 3bitrd 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ x e. X ) -> ( ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } <-> ( k X. { x } ) C_ v ) )
54 53 rabbidva 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } } = { x e. X | ( k X. { x } ) C_ v } )
55 sneq 
 |-  ( x = w -> { x } = { w } )
56 55 xpeq2d 
 |-  ( x = w -> ( k X. { x } ) = ( k X. { w } ) )
57 56 sseq1d 
 |-  ( x = w -> ( ( k X. { x } ) C_ v <-> ( k X. { w } ) C_ v ) )
58 57 elrab 
 |-  ( w e. { x e. X | ( k X. { x } ) C_ v } <-> ( w e. X /\ ( k X. { w } ) C_ v ) )
59 eqid 
 |-  U. ( S |`t k ) = U. ( S |`t k )
60 eqid 
 |-  U. R = U. R
61 simplr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( S |`t k ) e. Comp )
62 simpll 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) -> R e. ( TopOn ` X ) )
63 62 ad2antrr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> R e. ( TopOn ` X ) )
64 topontop 
 |-  ( R e. ( TopOn ` X ) -> R e. Top )
65 63 64 syl 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> R e. Top )
66 topontop 
 |-  ( S e. ( TopOn ` Y ) -> S e. Top )
67 66 adantl 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> S e. Top )
68 64 adantr 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> R e. Top )
69 txtop 
 |-  ( ( S e. Top /\ R e. Top ) -> ( S tX R ) e. Top )
70 67 68 69 syl2anc 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( S tX R ) e. Top )
71 70 ad3antrrr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( S tX R ) e. Top )
72 vex 
 |-  k e. _V
73 toponmax 
 |-  ( R e. ( TopOn ` X ) -> X e. R )
74 63 73 syl 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> X e. R )
75 xpexg 
 |-  ( ( k e. _V /\ X e. R ) -> ( k X. X ) e. _V )
76 72 74 75 sylancr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. X ) e. _V )
77 simprr 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) -> v e. ( S tX R ) )
78 77 ad2antrr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> v e. ( S tX R ) )
79 elrestr 
 |-  ( ( ( S tX R ) e. Top /\ ( k X. X ) e. _V /\ v e. ( S tX R ) ) -> ( v i^i ( k X. X ) ) e. ( ( S tX R ) |`t ( k X. X ) ) )
80 71 76 78 79 syl3anc 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( v i^i ( k X. X ) ) e. ( ( S tX R ) |`t ( k X. X ) ) )
81 67 ad3antrrr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> S e. Top )
82 72 a1i 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> k e. _V )
83 txrest 
 |-  ( ( ( S e. Top /\ R e. Top ) /\ ( k e. _V /\ X e. R ) ) -> ( ( S tX R ) |`t ( k X. X ) ) = ( ( S |`t k ) tX ( R |`t X ) ) )
84 81 65 82 74 83 syl22anc 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( ( S tX R ) |`t ( k X. X ) ) = ( ( S |`t k ) tX ( R |`t X ) ) )
85 toponuni 
 |-  ( R e. ( TopOn ` X ) -> X = U. R )
86 63 85 syl 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> X = U. R )
87 86 oveq2d 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( R |`t X ) = ( R |`t U. R ) )
88 60 restid 
 |-  ( R e. ( TopOn ` X ) -> ( R |`t U. R ) = R )
89 63 88 syl 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( R |`t U. R ) = R )
90 87 89 eqtrd 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( R |`t X ) = R )
91 90 oveq2d 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( ( S |`t k ) tX ( R |`t X ) ) = ( ( S |`t k ) tX R ) )
92 84 91 eqtrd 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( ( S tX R ) |`t ( k X. X ) ) = ( ( S |`t k ) tX R ) )
93 80 92 eleqtrd 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( v i^i ( k X. X ) ) e. ( ( S |`t k ) tX R ) )
94 23 adantr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> S e. ( TopOn ` Y ) )
95 26 adantr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> k C_ Y )
96 resttopon 
 |-  ( ( S e. ( TopOn ` Y ) /\ k C_ Y ) -> ( S |`t k ) e. ( TopOn ` k ) )
97 94 95 96 syl2anc 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( S |`t k ) e. ( TopOn ` k ) )
98 toponuni 
 |-  ( ( S |`t k ) e. ( TopOn ` k ) -> k = U. ( S |`t k ) )
99 97 98 syl 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> k = U. ( S |`t k ) )
100 99 xpeq1d 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. { w } ) = ( U. ( S |`t k ) X. { w } ) )
101 simprr 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. { w } ) C_ v )
102 simprl 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> w e. X )
103 102 snssd 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> { w } C_ X )
104 xpss2 
 |-  ( { w } C_ X -> ( k X. { w } ) C_ ( k X. X ) )
105 103 104 syl 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. { w } ) C_ ( k X. X ) )
106 101 105 ssind 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( k X. { w } ) C_ ( v i^i ( k X. X ) ) )
107 100 106 eqsstrrd 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( U. ( S |`t k ) X. { w } ) C_ ( v i^i ( k X. X ) ) )
108 102 86 eleqtrd 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> w e. U. R )
109 59 60 61 65 93 107 108 txtube 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> E. r e. R ( w e. r /\ ( U. ( S |`t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) )
110 toponss 
 |-  ( ( R e. ( TopOn ` X ) /\ r e. R ) -> r C_ X )
111 63 110 sylan 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> r C_ X )
112 ssrab 
 |-  ( r C_ { x e. X | ( k X. { x } ) C_ v } <-> ( r C_ X /\ A. x e. r ( k X. { x } ) C_ v ) )
113 112 baib 
 |-  ( r C_ X -> ( r C_ { x e. X | ( k X. { x } ) C_ v } <-> A. x e. r ( k X. { x } ) C_ v ) )
114 111 113 syl 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( r C_ { x e. X | ( k X. { x } ) C_ v } <-> A. x e. r ( k X. { x } ) C_ v ) )
115 xpss2 
 |-  ( r C_ X -> ( k X. r ) C_ ( k X. X ) )
116 111 115 syl 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( k X. r ) C_ ( k X. X ) )
117 116 biantrud 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( ( k X. r ) C_ v <-> ( ( k X. r ) C_ v /\ ( k X. r ) C_ ( k X. X ) ) ) )
118 iunid 
 |-  U_ x e. r { x } = r
119 118 xpeq2i 
 |-  ( k X. U_ x e. r { x } ) = ( k X. r )
120 xpiundi 
 |-  ( k X. U_ x e. r { x } ) = U_ x e. r ( k X. { x } )
121 119 120 eqtr3i 
 |-  ( k X. r ) = U_ x e. r ( k X. { x } )
122 121 sseq1i 
 |-  ( ( k X. r ) C_ v <-> U_ x e. r ( k X. { x } ) C_ v )
123 iunss 
 |-  ( U_ x e. r ( k X. { x } ) C_ v <-> A. x e. r ( k X. { x } ) C_ v )
124 122 123 bitri 
 |-  ( ( k X. r ) C_ v <-> A. x e. r ( k X. { x } ) C_ v )
125 ssin 
 |-  ( ( ( k X. r ) C_ v /\ ( k X. r ) C_ ( k X. X ) ) <-> ( k X. r ) C_ ( v i^i ( k X. X ) ) )
126 117 124 125 3bitr3g 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( A. x e. r ( k X. { x } ) C_ v <-> ( k X. r ) C_ ( v i^i ( k X. X ) ) ) )
127 99 adantr 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> k = U. ( S |`t k ) )
128 127 xpeq1d 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( k X. r ) = ( U. ( S |`t k ) X. r ) )
129 128 sseq1d 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( ( k X. r ) C_ ( v i^i ( k X. X ) ) <-> ( U. ( S |`t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) )
130 114 126 129 3bitrd 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( r C_ { x e. X | ( k X. { x } ) C_ v } <-> ( U. ( S |`t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) )
131 130 anbi2d 
 |-  ( ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) /\ r e. R ) -> ( ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) <-> ( w e. r /\ ( U. ( S |`t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) ) )
132 131 rexbidva 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> ( E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) <-> E. r e. R ( w e. r /\ ( U. ( S |`t k ) X. r ) C_ ( v i^i ( k X. X ) ) ) ) )
133 109 132 mpbird 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ ( w e. X /\ ( k X. { w } ) C_ v ) ) -> E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) )
134 58 133 sylan2b 
 |-  ( ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) /\ w e. { x e. X | ( k X. { x } ) C_ v } ) -> E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) )
135 134 ralrimiva 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> A. w e. { x e. X | ( k X. { x } ) C_ v } E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) )
136 eltop2 
 |-  ( R e. Top -> ( { x e. X | ( k X. { x } ) C_ v } e. R <-> A. w e. { x e. X | ( k X. { x } ) C_ v } E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) ) )
137 14 68 136 3syl 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> ( { x e. X | ( k X. { x } ) C_ v } e. R <-> A. w e. { x e. X | ( k X. { x } ) C_ v } E. r e. R ( w e. r /\ r C_ { x e. X | ( k X. { x } ) C_ v } ) ) )
138 135 137 mpbird 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> { x e. X | ( k X. { x } ) C_ v } e. R )
139 54 138 eqeltrd 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } } e. R )
140 imaeq2 
 |-  ( z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } -> ( `' F " z ) = ( `' F " { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) )
141 1 mptpreima 
 |-  ( `' F " { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) = { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } }
142 140 141 eqtrdi 
 |-  ( z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } -> ( `' F " z ) = { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } } )
143 142 eleq1d 
 |-  ( z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } -> ( ( `' F " z ) e. R <-> { x e. X | ( y e. Y |-> <. y , x >. ) e. { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } } e. R ) )
144 139 143 syl5ibrcom 
 |-  ( ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) /\ ( S |`t k ) e. Comp ) -> ( z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } -> ( `' F " z ) e. R ) )
145 144 expimpd 
 |-  ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( k e. ~P U. S /\ v e. ( S tX R ) ) ) -> ( ( ( S |`t k ) e. Comp /\ z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) -> ( `' F " z ) e. R ) )
146 145 rexlimdvva 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( E. k e. ~P U. S E. v e. ( S tX R ) ( ( S |`t k ) e. Comp /\ z = { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) -> ( `' F " z ) e. R ) )
147 13 146 syl5bi 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( z e. ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) -> ( `' F " z ) e. R ) )
148 147 ralrimiv 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> A. z e. ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) ( `' F " z ) e. R )
149 simpl 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> R e. ( TopOn ` X ) )
150 ovex 
 |-  ( S Cn ( S tX R ) ) e. _V
151 150 pwex 
 |-  ~P ( S Cn ( S tX R ) ) e. _V
152 9 10 11 xkotf 
 |-  ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) : ( { w e. ~P U. S | ( S |`t w ) e. Comp } X. ( S tX R ) ) --> ~P ( S Cn ( S tX R ) )
153 frn 
 |-  ( ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) : ( { w e. ~P U. S | ( S |`t w ) e. Comp } X. ( S tX R ) ) --> ~P ( S Cn ( S tX R ) ) -> ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) C_ ~P ( S Cn ( S tX R ) ) )
154 152 153 ax-mp 
 |-  ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) C_ ~P ( S Cn ( S tX R ) )
155 151 154 ssexi 
 |-  ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) e. _V
156 155 a1i 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) e. _V )
157 9 10 11 xkoval 
 |-  ( ( S e. Top /\ ( S tX R ) e. Top ) -> ( ( S tX R ) ^ko S ) = ( topGen ` ( fi ` ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) ) ) )
158 67 70 157 syl2anc 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( ( S tX R ) ^ko S ) = ( topGen ` ( fi ` ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) ) ) )
159 eqid 
 |-  ( ( S tX R ) ^ko S ) = ( ( S tX R ) ^ko S )
160 159 xkotopon 
 |-  ( ( S e. Top /\ ( S tX R ) e. Top ) -> ( ( S tX R ) ^ko S ) e. ( TopOn ` ( S Cn ( S tX R ) ) ) )
161 67 70 160 syl2anc 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( ( S tX R ) ^ko S ) e. ( TopOn ` ( S Cn ( S tX R ) ) ) )
162 149 156 158 161 subbascn 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( F e. ( R Cn ( ( S tX R ) ^ko S ) ) <-> ( F : X --> ( S Cn ( S tX R ) ) /\ A. z e. ran ( k e. { w e. ~P U. S | ( S |`t w ) e. Comp } , v e. ( S tX R ) |-> { f e. ( S Cn ( S tX R ) ) | ( f " k ) C_ v } ) ( `' F " z ) e. R ) ) )
163 8 148 162 mpbir2and 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> F e. ( R Cn ( ( S tX R ) ^ko S ) ) )