This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Top \land S \in Top) \to J \in TopOn (R Cn S)$

Step	Hyp	Ref	Expression
1		xkouni.1	$⊢ J = S^_{ko} R$
2		xkotop	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in Top$
3	1 2	eqeltrid	$⊢ (R \in Top \land S \in Top) \to J \in Top$
4	1	xkouni	$⊢ (R \in Top \land S \in Top) \to R Cn S = ⋃ J$
5		istopon	$⊢ J \in TopOn (R Cn S) \leftrightarrow (J \in Top \land R Cn S = ⋃ J)$
6	3 4 5	sylanbrc	$⊢ (R \in Top \land S \in Top) \to J \in TopOn (R Cn S)$