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 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 )