Metamath Proof Explorer

Theorem txtopon

Description: The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion txtopon ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → R × t S ∈ TopOn ⁡ X × Y

Proof

Step Hyp Ref Expression
1 topontop ⊢ R ∈ TopOn ⁡ X → R ∈ Top
2 topontop ⊢ S ∈ TopOn ⁡ Y → S ∈ Top
3 txtop ⊢ R ∈ Top ∧ S ∈ Top → R × t S ∈ Top
4 1 2 3 syl2an ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → R × t S ∈ Top
5 eqid ⊢ ran ⁡ u ∈ R , v ∈ S ⟼ u × v = ran ⁡ u ∈ R , v ∈ S ⟼ u × v
6 eqid ⊢ ⋃ R = ⋃ R
7 eqid ⊢ ⋃ S = ⋃ S
8 5 6 7 txuni2 ⊢ ⋃ R × ⋃ S = ⋃ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
9 toponuni ⊢ R ∈ TopOn ⁡ X → X = ⋃ R
10 toponuni ⊢ S ∈ TopOn ⁡ Y → Y = ⋃ S
11 xpeq12 ⊢ X = ⋃ R ∧ Y = ⋃ S → X × Y = ⋃ R × ⋃ S
12 9 10 11 syl2an ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → X × Y = ⋃ R × ⋃ S
13 5 txbasex ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ V
14 unitg ⊢ ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ V → ⋃ topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v = ⋃ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
15 13 14 syl ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → ⋃ topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v = ⋃ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
16 8 12 15 3eqtr4a ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → X × Y = ⋃ topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
17 5 txval ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → R × t S = topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
18 17 unieqd ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → ⋃ R × t S = ⋃ topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
19 16 18 eqtr4d ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → X × Y = ⋃ R × t S
20 istopon ⊢ R × t S ∈ TopOn ⁡ X × Y ↔ R × t S ∈ Top ∧ X × Y = ⋃ R × t S
21 4 19 20 sylanbrc ⊢ R ∈ TopOn ⁡ X ∧ S ∈ TopOn ⁡ Y → R × t S ∈ TopOn ⁡ X × Y