Description: The base set of the compact-open topology. (Contributed by Mario Carneiro, 22-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | xkouni.1 | |- J = ( S ^ko R ) |
|
Assertion | xkotopon | |- ( ( R e. Top /\ S e. Top ) -> J e. ( TopOn ` ( R Cn S ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xkouni.1 | |- J = ( S ^ko R ) |
|
2 | xkotop | |- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top ) |
|
3 | 1 2 | eqeltrid | |- ( ( R e. Top /\ S e. Top ) -> J e. Top ) |
4 | 1 | xkouni | |- ( ( R e. Top /\ S e. Top ) -> ( R Cn S ) = U. J ) |
5 | istopon | |- ( J e. ( TopOn ` ( R Cn S ) ) <-> ( J e. Top /\ ( R Cn S ) = U. J ) ) |
|
6 | 3 4 5 | sylanbrc | |- ( ( R e. Top /\ S e. Top ) -> J e. ( TopOn ` ( R Cn S ) ) ) |