Theorem xkotopon

Description: The base set of the compact-open topology. (Contributed by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypothesis	xkouni.1	⊢ 𝐽 = ( 𝑆 ↑ko 𝑅 )
Assertion	xkotopon	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝐽 ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xkouni.1	⊢ 𝐽 = ( 𝑆 ↑ko 𝑅 )
2		xkotop	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ Top )
3	1 2	eqeltrid	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝐽 ∈ Top )
4	1	xkouni	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 Cn 𝑆 ) = ∪ 𝐽 )
5		istopon	⊢ ( 𝐽 ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) ↔ ( 𝐽 ∈ Top ∧ ( 𝑅 Cn 𝑆 ) = ∪ 𝐽 ) )
6	3 4 5	sylanbrc	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝐽 ∈ ( TopOn ‘ ( 𝑅 Cn 𝑆 ) ) )