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 𝐵 = ran ( 𝑥𝑅 , 𝑦𝑆 ↦ ( 𝑥 × 𝑦 ) )
Assertion txbasex ( ( 𝑅𝑉𝑆𝑊 ) → 𝐵 ∈ V )

Proof

Step Hyp Ref Expression
1 txval.1 𝐵 = ran ( 𝑥𝑅 , 𝑦𝑆 ↦ ( 𝑥 × 𝑦 ) )
2 eqid 𝑅 = 𝑅
3 eqid 𝑆 = 𝑆
4 1 2 3 txuni2 ( 𝑅 × 𝑆 ) = 𝐵
5 uniexg ( 𝑅𝑉 𝑅 ∈ V )
6 uniexg ( 𝑆𝑊 𝑆 ∈ V )
7 xpexg ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑅 × 𝑆 ) ∈ V )
8 5 6 7 syl2an ( ( 𝑅𝑉𝑆𝑊 ) → ( 𝑅 × 𝑆 ) ∈ V )
9 4 8 eqeltrrid ( ( 𝑅𝑉𝑆𝑊 ) → 𝐵 ∈ V )
10 uniexb ( 𝐵 ∈ V ↔ 𝐵 ∈ V )
11 9 10 sylibr ( ( 𝑅𝑉𝑆𝑊 ) → 𝐵 ∈ V )