This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem txunii

Description: The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010)

Ref Expression
Hypotheses txunii.1 ⊢ R ∈ Top
txunii.2 ⊢ S ∈ Top
txunii.3 ⊢ X = ⋃ R
txunii.4 ⊢ Y = ⋃ S
Assertion txunii ⊢ X × Y = ⋃ R × t S

Proof

Step Hyp Ref Expression
1 txunii.1 ⊢ R ∈ Top
2 txunii.2 ⊢ S ∈ Top
3 txunii.3 ⊢ X = ⋃ R
4 txunii.4 ⊢ Y = ⋃ S
5 3 4 txuni ⊢ R ∈ Top ∧ S ∈ Top → X × Y = ⋃ R × t S
6 1 2 5 mp2an ⊢ X × Y = ⋃ R × t S