Metamath Proof Explorer

Theorem txopn

Description: The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion txopn ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 × 𝐵 ) ∈ ( 𝑅 ×t 𝑆 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) )
2 1 txbasex ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ V )
3 bastg ⊢ ( ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ∈ V → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ⊆ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
4 2 3 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ⊆ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
5 4 adantr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ⊆ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
6 eqid ⊢ ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 )
7 xpeq1 ⊢ ( 𝑢 = 𝐴 → ( 𝑢 × 𝑣 ) = ( 𝐴 × 𝑣 ) )
8 7 eqeq2d ⊢ ( 𝑢 = 𝐴 → ( ( 𝐴 × 𝐵 ) = ( 𝑢 × 𝑣 ) ↔ ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝑣 ) ) )
9 xpeq2 ⊢ ( 𝑣 = 𝐵 → ( 𝐴 × 𝑣 ) = ( 𝐴 × 𝐵 ) )
10 9 eqeq2d ⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝑣 ) ↔ ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) ) )
11 8 10 rspc2ev ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ( 𝐴 × 𝐵 ) = ( 𝐴 × 𝐵 ) ) → ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝐴 × 𝐵 ) = ( 𝑢 × 𝑣 ) )
12 6 11 mp3an3 ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝐴 × 𝐵 ) = ( 𝑢 × 𝑣 ) )
13 xpexg ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 × 𝐵 ) ∈ V )
14 eqid ⊢ ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) = ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) )
15 14 elrnmpog ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( ( 𝐴 × 𝐵 ) ∈ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ↔ ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝐴 × 𝐵 ) = ( 𝑢 × 𝑣 ) ) )
16 13 15 syl ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 × 𝐵 ) ∈ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ↔ ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝐴 × 𝐵 ) = ( 𝑢 × 𝑣 ) ) )
17 12 16 mpbird ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 × 𝐵 ) ∈ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) )
18 17 adantl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 × 𝐵 ) ∈ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) )
19 5 18 sseldd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 × 𝐵 ) ∈ ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
20 1 txval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
21 20 adantr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑆 ↦ ( 𝑢 × 𝑣 ) ) ) )
22 19 21 eleqtrrd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 × 𝐵 ) ∈ ( 𝑅 ×t 𝑆 ) )