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 V K W S J × t K p S x J y K p x × y x × y S

Proof

Step Hyp Ref Expression
1 eqid ran x J , y K x × y = ran x J , y K x × y
2 1 txval J V K W J × t K = topGen ran x J , y K x × y
3 2 eleq2d J V K W S J × t K S topGen ran x J , y K x × y
4 1 txbasex J V K W ran x J , y K x × y V
5 eltg2b ran x J , y K x × y V S topGen ran x J , y K x × y p S z ran x J , y K x × y p z z S
6 4 5 syl J V K W S topGen ran x J , y K x × y p S z ran x J , y K x × y p z z S
7 vex x V
8 vex y V
9 7 8 xpex x × y V
10 9 rgen2w x J y K x × y V
11 eqid x J , y K x × y = x J , y K x × y
12 eleq2 z = x × y p z p x × y
13 sseq1 z = x × y z S x × y S
14 12 13 anbi12d z = x × y p z z S p x × y x × y S
15 11 14 rexrnmpo x J y K x × y V z ran x J , y K x × y p z z S x J y K p x × y x × y S
16 10 15 ax-mp z ran x J , y K x × y p z z S x J y K p x × y x × y S
17 16 ralbii p S z ran x J , y K x × y p z z S p S x J y K p x × y x × y S
18 6 17 bitrdi J V K W S topGen ran x J , y K x × y p S x J y K p x × y x × y S
19 3 18 bitrd J V K W S J × t K p S x J y K p x × y x × y S