# 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 ${⊢}\left({R}\in \mathrm{Top}\wedge {S}\in \mathrm{Top}\right)\to {R}{×}_{t}{S}\in \mathrm{Top}$

### Proof

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