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 ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 topontop ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑅 ∈ Top )
2 topontop ⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑆 ∈ Top )
3 txtop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
4 1 2 3 syl2an ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
5 eqid ⊢ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) )
6 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
7 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
8 5 6 7 txuni2 ⊢ ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) )
9 toponuni ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝑅 )
10 toponuni ⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝑆 )
11 xpeq12 ⊢ ( ( 𝑋 = ∪ 𝑅 ∧ 𝑌 = ∪ 𝑆 ) → ( 𝑋 × 𝑌 ) = ( ∪ 𝑅 × ∪ 𝑆 ) )
12 9 10 11 syl2an ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ( ∪ 𝑅 × ∪ 𝑆 ) )
13 5 txbasex ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ V )
14 unitg ⊢ ( ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ V → ∪ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) = ∪ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) )
15 13 14 syl ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ∪ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) = ∪ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) )
16 8 12 15 3eqtr4a ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
17 5 txval ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
18 17 unieqd ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
19 16 18 eqtr4d ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
20 istopon ⊢ ( ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) ) )
21 4 19 20 sylanbrc ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )