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\times 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\times y\right)$$
2		eqid	$$⊢\bigcup R=\bigcup R$$
3		eqid	$$⊢\bigcup S=\bigcup S$$
4	1 2 3	txuni2	$$⊢\bigcup R\times \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\times \bigcup S\in \mathrm{V}$$
8	5 6 7	syl2an	$$⊢\left(R\in V\wedge S\in W\right)\to \bigcup R\times \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}\leftrightarrow \bigcup B\in \mathrm{V}$$
11	9 10	sylibr	$$⊢\left(R\in V\wedge S\in W\right)\to B\in \mathrm{V}$$