Metamath Proof Explorer

Theorem txtop

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

Ref Expression
Assertion txtop ⊢ R ∈ Top ∧ S ∈ Top → R × t S ∈ Top

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ⁡ u ∈ R , v ∈ S ⟼ u × v = ran ⁡ u ∈ R , v ∈ S ⟼ u × v
2 1 txval ⊢ R ∈ Top ∧ S ∈ Top → R × t S = topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
3 topbas ⊢ R ∈ Top → R ∈ TopBases
4 topbas ⊢ S ∈ Top → S ∈ TopBases
5 1 txbas ⊢ R ∈ TopBases ∧ S ∈ TopBases → ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ TopBases
6 3 4 5 syl2an ⊢ R ∈ Top ∧ S ∈ Top → ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ TopBases
7 tgcl ⊢ ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ TopBases → topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ Top
8 6 7 syl ⊢ R ∈ Top ∧ S ∈ Top → topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ Top
9 2 8 eqeltrd ⊢ R ∈ Top ∧ S ∈ Top → R × t S ∈ Top