# 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}=\mathrm{ran}\left({x}\in {R},{y}\in {S}⟼{x}×{y}\right)$
Assertion txbasex ${⊢}\left({R}\in {V}\wedge {S}\in {W}\right)\to {B}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 txval.1 ${⊢}{B}=\mathrm{ran}\left({x}\in {R},{y}\in {S}⟼{x}×{y}\right)$
2 eqid ${⊢}\bigcup {R}=\bigcup {R}$
3 eqid ${⊢}\bigcup {S}=\bigcup {S}$
4 1 2 3 txuni2 ${⊢}\bigcup {R}×\bigcup {S}=\bigcup {B}$
5 uniexg ${⊢}{R}\in {V}\to \bigcup {R}\in \mathrm{V}$
6 uniexg ${⊢}{S}\in {W}\to \bigcup {S}\in \mathrm{V}$
7 xpexg ${⊢}\left(\bigcup {R}\in \mathrm{V}\wedge \bigcup {S}\in \mathrm{V}\right)\to \bigcup {R}×\bigcup {S}\in \mathrm{V}$
8 5 6 7 syl2an ${⊢}\left({R}\in {V}\wedge {S}\in {W}\right)\to \bigcup {R}×\bigcup {S}\in \mathrm{V}$
9 4 8 eqeltrrid ${⊢}\left({R}\in {V}\wedge {S}\in {W}\right)\to \bigcup {B}\in \mathrm{V}$
10 uniexb ${⊢}{B}\in \mathrm{V}↔\bigcup {B}\in \mathrm{V}$
11 9 10 sylibr ${⊢}\left({R}\in {V}\wedge {S}\in {W}\right)\to {B}\in \mathrm{V}$