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 = TopOpen (R)$
	xpstopn.k	$⊢ K = TopOpen (S)$
	xpstopn.o	$⊢ O = TopOpen (T)$
Assertion	xpstopn	$⊢ (R \in TopSp \land S \in TopSp) \to O = J \times_{t} K$

Proof

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

Metamath Proof Explorer

Theorem xpstopn

Proof