Step |
Hyp |
Ref |
Expression |
1 |
|
xkococn.1 |
|- F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) ) |
2 |
|
simprr |
|- ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( f e. ( S Cn T ) /\ g e. ( R Cn S ) ) ) -> g e. ( R Cn S ) ) |
3 |
|
simprl |
|- ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( f e. ( S Cn T ) /\ g e. ( R Cn S ) ) ) -> f e. ( S Cn T ) ) |
4 |
|
cnco |
|- ( ( g e. ( R Cn S ) /\ f e. ( S Cn T ) ) -> ( f o. g ) e. ( R Cn T ) ) |
5 |
2 3 4
|
syl2anc |
|- ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( f e. ( S Cn T ) /\ g e. ( R Cn S ) ) ) -> ( f o. g ) e. ( R Cn T ) ) |
6 |
5
|
ralrimivva |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> A. f e. ( S Cn T ) A. g e. ( R Cn S ) ( f o. g ) e. ( R Cn T ) ) |
7 |
1
|
fmpo |
|- ( A. f e. ( S Cn T ) A. g e. ( R Cn S ) ( f o. g ) e. ( R Cn T ) <-> F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) ) |
8 |
6 7
|
sylib |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) ) |
9 |
|
eqid |
|- ( 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 } ) |
10 |
9
|
rnmpo |
|- 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. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } } |
11 |
10
|
eleq2i |
|- ( 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 } ) <-> x e. { x | E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } } ) |
12 |
|
abid |
|- ( x e. { x | E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } } <-> E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) |
13 |
|
oveq2 |
|- ( y = k -> ( R |`t y ) = ( R |`t k ) ) |
14 |
13
|
eleq1d |
|- ( y = k -> ( ( R |`t y ) e. Comp <-> ( R |`t k ) e. Comp ) ) |
15 |
14
|
rexrab |
|- ( E. k e. { y e. ~P U. R | ( R |`t y ) e. Comp } E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } <-> E. k e. ~P U. R ( ( R |`t k ) e. Comp /\ E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) |
16 |
11 12 15
|
3bitri |
|- ( 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 ( ( R |`t k ) e. Comp /\ E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) |
17 |
8
|
ad2antrr |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) ) |
18 |
|
ffn |
|- ( F : ( ( S Cn T ) X. ( R Cn S ) ) --> ( R Cn T ) -> F Fn ( ( S Cn T ) X. ( R Cn S ) ) ) |
19 |
|
elpreima |
|- ( F Fn ( ( S Cn T ) X. ( R Cn S ) ) -> ( y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) <-> ( y e. ( ( S Cn T ) X. ( R Cn S ) ) /\ ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) |
20 |
17 18 19
|
3syl |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) <-> ( y e. ( ( S Cn T ) X. ( R Cn S ) ) /\ ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) |
21 |
|
coeq1 |
|- ( f = a -> ( f o. g ) = ( a o. g ) ) |
22 |
|
coeq2 |
|- ( g = b -> ( a o. g ) = ( a o. b ) ) |
23 |
|
vex |
|- a e. _V |
24 |
|
vex |
|- b e. _V |
25 |
23 24
|
coex |
|- ( a o. b ) e. _V |
26 |
21 22 1 25
|
ovmpo |
|- ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) -> ( a F b ) = ( a o. b ) ) |
27 |
26
|
adantl |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( a F b ) = ( a o. b ) ) |
28 |
27
|
eleq1d |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( a o. b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) |
29 |
|
imaeq1 |
|- ( h = ( a o. b ) -> ( h " k ) = ( ( a o. b ) " k ) ) |
30 |
29
|
sseq1d |
|- ( h = ( a o. b ) -> ( ( h " k ) C_ v <-> ( ( a o. b ) " k ) C_ v ) ) |
31 |
30
|
elrab |
|- ( ( a o. b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( ( a o. b ) e. ( R Cn T ) /\ ( ( a o. b ) " k ) C_ v ) ) |
32 |
31
|
simprbi |
|- ( ( a o. b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( ( a o. b ) " k ) C_ v ) |
33 |
|
simp2 |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> S e. N-Locally Comp ) |
34 |
33
|
ad3antrrr |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> S e. N-Locally Comp ) |
35 |
|
elpwi |
|- ( k e. ~P U. R -> k C_ U. R ) |
36 |
35
|
ad2antrl |
|- ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) -> k C_ U. R ) |
37 |
36
|
ad2antrr |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> k C_ U. R ) |
38 |
|
simprr |
|- ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) -> ( R |`t k ) e. Comp ) |
39 |
38
|
ad2antrr |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> ( R |`t k ) e. Comp ) |
40 |
|
simplr |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> v e. T ) |
41 |
|
simprll |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> a e. ( S Cn T ) ) |
42 |
|
simprlr |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> b e. ( R Cn S ) ) |
43 |
|
simprr |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> ( ( a o. b ) " k ) C_ v ) |
44 |
1 34 37 39 40 41 42 43
|
xkococnlem |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) /\ ( ( a o. b ) " k ) C_ v ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) |
45 |
44
|
expr |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( ( ( a o. b ) " k ) C_ v -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
46 |
32 45
|
syl5 |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( ( a o. b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
47 |
28 46
|
sylbid |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ ( a e. ( S Cn T ) /\ b e. ( R Cn S ) ) ) -> ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
48 |
47
|
ralrimivva |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> A. a e. ( S Cn T ) A. b e. ( R Cn S ) ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
49 |
|
fveq2 |
|- ( y = <. a , b >. -> ( F ` y ) = ( F ` <. a , b >. ) ) |
50 |
|
df-ov |
|- ( a F b ) = ( F ` <. a , b >. ) |
51 |
49 50
|
eqtr4di |
|- ( y = <. a , b >. -> ( F ` y ) = ( a F b ) ) |
52 |
51
|
eleq1d |
|- ( y = <. a , b >. -> ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } <-> ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) |
53 |
|
eleq1 |
|- ( y = <. a , b >. -> ( y e. z <-> <. a , b >. e. z ) ) |
54 |
53
|
anbi1d |
|- ( y = <. a , b >. -> ( ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) <-> ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
55 |
54
|
rexbidv |
|- ( y = <. a , b >. -> ( E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) <-> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
56 |
52 55
|
imbi12d |
|- ( y = <. a , b >. -> ( ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) <-> ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) ) |
57 |
56
|
ralxp |
|- ( A. y e. ( ( S Cn T ) X. ( R Cn S ) ) ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) <-> A. a e. ( S Cn T ) A. b e. ( R Cn S ) ( ( a F b ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. a , b >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
58 |
48 57
|
sylibr |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> A. y e. ( ( S Cn T ) X. ( R Cn S ) ) ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
59 |
58
|
r19.21bi |
|- ( ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) /\ y e. ( ( S Cn T ) X. ( R Cn S ) ) ) -> ( ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
60 |
59
|
expimpd |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( ( y e. ( ( S Cn T ) X. ( R Cn S ) ) /\ ( F ` y ) e. { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
61 |
20 60
|
sylbid |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
62 |
61
|
ralrimiv |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> A. y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) |
63 |
|
nllytop |
|- ( S e. N-Locally Comp -> S e. Top ) |
64 |
63
|
3ad2ant2 |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> S e. Top ) |
65 |
|
simp3 |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> T e. Top ) |
66 |
|
xkotop |
|- ( ( S e. Top /\ T e. Top ) -> ( T ^ko S ) e. Top ) |
67 |
64 65 66
|
syl2anc |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( T ^ko S ) e. Top ) |
68 |
|
simp1 |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> R e. Top ) |
69 |
|
xkotop |
|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top ) |
70 |
68 64 69
|
syl2anc |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( S ^ko R ) e. Top ) |
71 |
|
txtop |
|- ( ( ( T ^ko S ) e. Top /\ ( S ^ko R ) e. Top ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. Top ) |
72 |
67 70 71
|
syl2anc |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. Top ) |
73 |
72
|
ad2antrr |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. Top ) |
74 |
|
eltop2 |
|- ( ( ( T ^ko S ) tX ( S ^ko R ) ) e. Top -> ( ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) <-> A. y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
75 |
73 74
|
syl |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) <-> A. y e. ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( y e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) ) ) |
76 |
62 75
|
mpbird |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) |
77 |
|
imaeq2 |
|- ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' F " x ) = ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) ) |
78 |
77
|
eleq1d |
|- ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) <-> ( `' F " { h e. ( R Cn T ) | ( h " k ) C_ v } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) |
79 |
76 78
|
syl5ibrcom |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) /\ v e. T ) -> ( x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) |
80 |
79
|
rexlimdva |
|- ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ ( k e. ~P U. R /\ ( R |`t k ) e. Comp ) ) -> ( E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) |
81 |
80
|
anassrs |
|- ( ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ k e. ~P U. R ) /\ ( R |`t k ) e. Comp ) -> ( E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) |
82 |
81
|
expimpd |
|- ( ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) /\ k e. ~P U. R ) -> ( ( ( R |`t k ) e. Comp /\ E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) |
83 |
82
|
rexlimdva |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( E. k e. ~P U. R ( ( R |`t k ) e. Comp /\ E. v e. T x = { h e. ( R Cn T ) | ( h " k ) C_ v } ) -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) |
84 |
16 83
|
syl5bi |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( 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 } ) -> ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) |
85 |
84
|
ralrimiv |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> 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 } ) ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) |
86 |
|
eqid |
|- ( T ^ko S ) = ( T ^ko S ) |
87 |
86
|
xkotopon |
|- ( ( S e. Top /\ T e. Top ) -> ( T ^ko S ) e. ( TopOn ` ( S Cn T ) ) ) |
88 |
64 65 87
|
syl2anc |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( T ^ko S ) e. ( TopOn ` ( S Cn T ) ) ) |
89 |
|
eqid |
|- ( S ^ko R ) = ( S ^ko R ) |
90 |
89
|
xkotopon |
|- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) ) |
91 |
68 64 90
|
syl2anc |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) ) |
92 |
|
txtopon |
|- ( ( ( T ^ko S ) e. ( TopOn ` ( S Cn T ) ) /\ ( S ^ko R ) e. ( TopOn ` ( R Cn S ) ) ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. ( TopOn ` ( ( S Cn T ) X. ( R Cn S ) ) ) ) |
93 |
88 91 92
|
syl2anc |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( ( T ^ko S ) tX ( S ^ko R ) ) e. ( TopOn ` ( ( S Cn T ) X. ( R Cn S ) ) ) ) |
94 |
|
ovex |
|- ( R Cn T ) e. _V |
95 |
94
|
pwex |
|- ~P ( R Cn T ) e. _V |
96 |
|
eqid |
|- U. R = U. R |
97 |
|
eqid |
|- { y e. ~P U. R | ( R |`t y ) e. Comp } = { y e. ~P U. R | ( R |`t y ) e. Comp } |
98 |
96 97 9
|
xkotf |
|- ( 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 ) |
99 |
|
frn |
|- ( ( 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 ) ) |
100 |
98 99
|
ax-mp |
|- 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 ) |
101 |
95 100
|
ssexi |
|- 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 |
102 |
101
|
a1i |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> 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 ) |
103 |
96 97 9
|
xkoval |
|- ( ( 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 } ) ) ) ) |
104 |
103
|
3adant2 |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ 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 } ) ) ) ) |
105 |
|
eqid |
|- ( T ^ko R ) = ( T ^ko R ) |
106 |
105
|
xkotopon |
|- ( ( R e. Top /\ T e. Top ) -> ( T ^ko R ) e. ( TopOn ` ( R Cn T ) ) ) |
107 |
106
|
3adant2 |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( T ^ko R ) e. ( TopOn ` ( R Cn T ) ) ) |
108 |
93 102 104 107
|
subbascn |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> ( F e. ( ( ( T ^ko S ) tX ( S ^ko R ) ) Cn ( T ^ko R ) ) <-> ( F : ( ( S Cn T ) X. ( 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 } ) ( `' F " x ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) ) ) ) |
109 |
8 85 108
|
mpbir2and |
|- ( ( R e. Top /\ S e. N-Locally Comp /\ T e. Top ) -> F e. ( ( ( T ^ko S ) tX ( S ^ko R ) ) Cn ( T ^ko R ) ) ) |