Theorem xpstopn

Description: The topology on a binary product of topological spaces, as we have defined it (transferring the indexed product topology on functions on { (/) , 1o } to ( X X. Y ) by the canonical bijection), coincides with the usual topological product (generated by a base of rectangles). (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	xpstps.t	⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
	xpstopn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
	xpstopn.k	⊢ 𝐾 = ( TopOpen ‘ 𝑆 )
	xpstopn.o	⊢ 𝑂 = ( TopOpen ‘ 𝑇 )
Assertion	xpstopn	⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑂 = ( 𝐽 ×t 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		xpstps.t	⊢ 𝑇 = ( 𝑅 ×s 𝑆 )
2		xpstopn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑅 )
3		xpstopn.k	⊢ 𝐾 = ( TopOpen ‘ 𝑆 )
4		xpstopn.o	⊢ 𝑂 = ( TopOpen ‘ 𝑇 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑆 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
8	1 2 3 4 5 6 7	xpstopnlem2	⊢ ( ( 𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp ) → 𝑂 = ( 𝐽 ×t 𝐾 ) )