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 e. R , y e. S |-> ( x X. y ) )
Assertion	txbasex	|- ( ( R e. V /\ S e. W ) -> B e. _V )

Proof

Step	Hyp	Ref	Expression
1		txval.1	|- B = ran ( x e. R , y e. S |-> ( x X. y ) )
2		eqid	|- U. R = U. R
3		eqid	|- U. S = U. S
4	1 2 3	txuni2	|- ( U. R X. U. S ) = U. B
5		uniexg	|- ( R e. V -> U. R e. _V )
6		uniexg	|- ( S e. W -> U. S e. _V )
7		xpexg	|- ( ( U. R e. _V /\ U. S e. _V ) -> ( U. R X. U. S ) e. _V )
8	5 6 7	syl2an	|- ( ( R e. V /\ S e. W ) -> ( U. R X. U. S ) e. _V )
9	4 8	eqeltrrid	|- ( ( R e. V /\ S e. W ) -> U. B e. _V )
10		uniexb	|- ( B e. _V <-> U. B e. _V )
11	9 10	sylibr	|- ( ( R e. V /\ S e. W ) -> B e. _V )