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