Metamath Proof Explorer


Theorem xkotopon

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 ) ) )

Proof

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 ) ) )