txuni

Description: The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	txuni.1	$⊢ X = ⋃ R$
	txuni.2	$⊢ Y = ⋃ S$
Assertion	txuni	$⊢ (R \in Top \land S \in Top) \to X \times Y = ⋃ (R \times_{t} S)$

Step	Hyp	Ref	Expression
1		txuni.1	$⊢ X = ⋃ R$
2		txuni.2	$⊢ Y = ⋃ S$
3	1	toptopon	$⊢ R \in Top \leftrightarrow R \in TopOn (X)$
4	2	toptopon	$⊢ S \in Top \leftrightarrow S \in TopOn (Y)$
5		txtopon	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to R \times_{t} S \in TopOn (X \times Y)$
6	3 4 5	syl2anb	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S \in TopOn (X \times Y)$
7		toponuni	$⊢ R \times_{t} S \in TopOn (X \times Y) \to X \times Y = ⋃ (R \times_{t} S)$
8	6 7	syl	$⊢ (R \in Top \land S \in Top) \to X \times Y = ⋃ (R \times_{t} S)$

Metamath Proof Explorer