This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem txbasex

Description: The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypothesis txval.1 ⊢ B = ran ⁡ x ∈ R , y ∈ S ⟼ x × y
Assertion txbasex ⊢ R ∈ V ∧ S ∈ W → B ∈ V

Proof

Step Hyp Ref Expression
1 txval.1 ⊢ B = ran ⁡ x ∈ R , y ∈ S ⟼ x × y
2 eqid ⊢ ⋃ R = ⋃ R
3 eqid ⊢ ⋃ S = ⋃ S
4 1 2 3 txuni2 ⊢ ⋃ R × ⋃ S = ⋃ B
5 uniexg ⊢ R ∈ V → ⋃ R ∈ V
6 uniexg ⊢ S ∈ W → ⋃ S ∈ V
7 xpexg ⊢ ⋃ R ∈ V ∧ ⋃ S ∈ V → ⋃ R × ⋃ S ∈ V
8 5 6 7 syl2an ⊢ R ∈ V ∧ S ∈ W → ⋃ R × ⋃ S ∈ V
9 4 8 eqeltrrid ⊢ R ∈ V ∧ S ∈ W → ⋃ B ∈ V
10 uniexb ⊢ B ∈ V ↔ ⋃ B ∈ V
11 9 10 sylibr ⊢ R ∈ V ∧ S ∈ W → B ∈ V