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 ⊢ R ∈ V ∧ S ∈ W ∧ A ∈ R ∧ B ∈ S → A × B ∈ R × t S

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ⁡ u ∈ R , v ∈ S ⟼ u × v = ran ⁡ u ∈ R , v ∈ S ⟼ u × v
2 1 txbasex ⊢ R ∈ V ∧ S ∈ W → ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ V
3 bastg ⊢ ran ⁡ u ∈ R , v ∈ S ⟼ u × v ∈ V → ran ⁡ u ∈ R , v ∈ S ⟼ u × v ⊆ topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
4 2 3 syl ⊢ R ∈ V ∧ S ∈ W → ran ⁡ u ∈ R , v ∈ S ⟼ u × v ⊆ topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
5 4 adantr ⊢ R ∈ V ∧ S ∈ W ∧ A ∈ R ∧ B ∈ S → ran ⁡ u ∈ R , v ∈ S ⟼ u × v ⊆ topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
6 eqid ⊢ A × B = A × B
7 xpeq1 ⊢ u = A → u × v = A × v
8 7 eqeq2d ⊢ u = A → A × B = u × v ↔ A × B = A × v
9 xpeq2 ⊢ v = B → A × v = A × B
10 9 eqeq2d ⊢ v = B → A × B = A × v ↔ A × B = A × B
11 8 10 rspc2ev ⊢ A ∈ R ∧ B ∈ S ∧ A × B = A × B → ∃ u ∈ R ∃ v ∈ S A × B = u × v
12 6 11 mp3an3 ⊢ A ∈ R ∧ B ∈ S → ∃ u ∈ R ∃ v ∈ S A × B = u × v
13 xpexg ⊢ A ∈ R ∧ B ∈ S → A × B ∈ V
14 eqid ⊢ u ∈ R , v ∈ S ⟼ u × v = u ∈ R , v ∈ S ⟼ u × v
15 14 elrnmpog ⊢ A × B ∈ V → A × B ∈ ran ⁡ u ∈ R , v ∈ S ⟼ u × v ↔ ∃ u ∈ R ∃ v ∈ S A × B = u × v
16 13 15 syl ⊢ A ∈ R ∧ B ∈ S → A × B ∈ ran ⁡ u ∈ R , v ∈ S ⟼ u × v ↔ ∃ u ∈ R ∃ v ∈ S A × B = u × v
17 12 16 mpbird ⊢ A ∈ R ∧ B ∈ S → A × B ∈ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
18 17 adantl ⊢ R ∈ V ∧ S ∈ W ∧ A ∈ R ∧ B ∈ S → A × B ∈ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
19 5 18 sseldd ⊢ R ∈ V ∧ S ∈ W ∧ A ∈ R ∧ B ∈ S → A × B ∈ topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
20 1 txval ⊢ R ∈ V ∧ S ∈ W → R × t S = topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
21 20 adantr ⊢ R ∈ V ∧ S ∈ W ∧ A ∈ R ∧ B ∈ S → R × t S = topGen ⁡ ran ⁡ u ∈ R , v ∈ S ⟼ u × v
22 19 21 eleqtrrd ⊢ R ∈ V ∧ S ∈ W ∧ A ∈ R ∧ B ∈ S → A × B ∈ R × t S