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	$$⊢T=R{\times }_{𝑠}S$$
	xpstopn.j	$$⊢J=\mathrm{TopOpen}\left(R\right)$$
	xpstopn.k	$$⊢K=\mathrm{TopOpen}\left(S\right)$$
	xpstopn.o	$$⊢O=\mathrm{TopOpen}\left(T\right)$$
Assertion	xpstopn	$$⊢\left(R\in \mathrm{TopSp}\wedge S\in \mathrm{TopSp}\right)\to O=J{\times }_{t}K$$

Proof

Step	Hyp	Ref	Expression
1		xpstps.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpstopn.j	$$⊢J=\mathrm{TopOpen}\left(R\right)$$
3		xpstopn.k	$$⊢K=\mathrm{TopOpen}\left(S\right)$$
4		xpstopn.o	$$⊢O=\mathrm{TopOpen}\left(T\right)$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
7		eqid	$$⊢\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)=\left(x\in {\mathrm{Base}}_R,y\in {\mathrm{Base}}_S⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
8	1 2 3 4 5 6 7	xpstopnlem2	$$⊢\left(R\in \mathrm{TopSp}\wedge S\in \mathrm{TopSp}\right)\to O=J{\times }_{t}K$$