Theorem txtop

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

	Ref	Expression
Assertion	txtop	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) )
2	1	txval	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
3		topbas	⊢ ( 𝑅 ∈ Top → 𝑅 ∈ TopBases )
4		topbas	⊢ ( 𝑆 ∈ Top → 𝑆 ∈ TopBases )
5	1	txbas	⊢ ( ( 𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ TopBases )
6	3 4 5	syl2an	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ TopBases )
7		tgcl	⊢ ( ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ TopBases → ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ∈ Top )
8	6 7	syl	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) ∈ Top )
9	2 8	eqeltrd	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )