txtop

Description: The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	txtop	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in Top$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran (u \in R, v \in S ⟼ u \times v) = ran (u \in R, v \in S ⟼ u \times v)$
2	1	txval	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S = topGen (ran (u \in R, v \in S ⟼ u \times v))$
3		topbas	$⊢ R \in Top \to R \in TopBases$
4		topbas	$⊢ S \in Top \to S \in TopBases$
5	1	txbas	$⊢ (R \in TopBases \land S \in TopBases) \to ran (u \in R, v \in S ⟼ u \times v) \in TopBases$
6	3 4 5	syl2an	$⊢ (R \in Top \land S \in Top) \to ran (u \in R, v \in S ⟼ u \times v) \in TopBases$
7		tgcl	$⊢ ran (u \in R, v \in S ⟼ u \times v) \in TopBases \to topGen (ran (u \in R, v \in S ⟼ u \times v)) \in Top$
8	6 7	syl	$⊢ (R \in Top \land S \in Top) \to topGen (ran (u \in R, v \in S ⟼ u \times v)) \in Top$
9	2 8	eqeltrd	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in Top$

Metamath Proof Explorer