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 ‘ ( 𝑋 × 𝑌 ) ) )