Metamath Proof Explorer

Theorem eltx

Description: A set in a product is open iff each point is surrounded by an open rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion eltx 
|- ( ( J e. V /\ K e. W ) -> ( S e. ( J tX K ) <-> A. p e. S E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran ( x e. J , y e. K |-> ( x X. y ) ) = ran ( x e. J , y e. K |-> ( x X. y ) )
2 1 txval 
 |-  ( ( J e. V /\ K e. W ) -> ( J tX K ) = ( topGen ` ran ( x e. J , y e. K |-> ( x X. y ) ) ) )
3 2 eleq2d 
 |-  ( ( J e. V /\ K e. W ) -> ( S e. ( J tX K ) <-> S e. ( topGen ` ran ( x e. J , y e. K |-> ( x X. y ) ) ) ) )
4 1 txbasex 
 |-  ( ( J e. V /\ K e. W ) -> ran ( x e. J , y e. K |-> ( x X. y ) ) e. _V )
5 eltg2b 
 |-  ( ran ( x e. J , y e. K |-> ( x X. y ) ) e. _V -> ( S e. ( topGen ` ran ( x e. J , y e. K |-> ( x X. y ) ) ) <-> A. p e. S E. z e. ran ( x e. J , y e. K |-> ( x X. y ) ) ( p e. z /\ z C_ S ) ) )
6 4 5 syl 
 |-  ( ( J e. V /\ K e. W ) -> ( S e. ( topGen ` ran ( x e. J , y e. K |-> ( x X. y ) ) ) <-> A. p e. S E. z e. ran ( x e. J , y e. K |-> ( x X. y ) ) ( p e. z /\ z C_ S ) ) )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 xpex 
 |-  ( x X. y ) e. _V
10 9 rgen2w 
 |-  A. x e. J A. y e. K ( x X. y ) e. _V
11 eqid 
 |-  ( x e. J , y e. K |-> ( x X. y ) ) = ( x e. J , y e. K |-> ( x X. y ) )
12 eleq2 
 |-  ( z = ( x X. y ) -> ( p e. z <-> p e. ( x X. y ) ) )
13 sseq1 
 |-  ( z = ( x X. y ) -> ( z C_ S <-> ( x X. y ) C_ S ) )
14 12 13 anbi12d 
 |-  ( z = ( x X. y ) -> ( ( p e. z /\ z C_ S ) <-> ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) ) )
15 11 14 rexrnmpo 
 |-  ( A. x e. J A. y e. K ( x X. y ) e. _V -> ( E. z e. ran ( x e. J , y e. K |-> ( x X. y ) ) ( p e. z /\ z C_ S ) <-> E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) ) )
16 10 15 ax-mp 
 |-  ( E. z e. ran ( x e. J , y e. K |-> ( x X. y ) ) ( p e. z /\ z C_ S ) <-> E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) )
17 16 ralbii 
 |-  ( A. p e. S E. z e. ran ( x e. J , y e. K |-> ( x X. y ) ) ( p e. z /\ z C_ S ) <-> A. p e. S E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) )
18 6 17 bitrdi 
 |-  ( ( J e. V /\ K e. W ) -> ( S e. ( topGen ` ran ( x e. J , y e. K |-> ( x X. y ) ) ) <-> A. p e. S E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) ) )
19 3 18 bitrd 
 |-  ( ( J e. V /\ K e. W ) -> ( S e. ( J tX K ) <-> A. p e. S E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) ) )