# 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 ${⊢}\left({J}\in {V}\wedge {K}\in {W}\right)\to \left({S}\in \left({J}{×}_{t}{K}\right)↔\forall {p}\in {S}\phantom{\rule{.4em}{0ex}}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({p}\in \left({x}×{y}\right)\wedge {x}×{y}\subseteq {S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)=\mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)$
2 1 txval ${⊢}\left({J}\in {V}\wedge {K}\in {W}\right)\to {J}{×}_{t}{K}=\mathrm{topGen}\left(\mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\right)$
3 2 eleq2d ${⊢}\left({J}\in {V}\wedge {K}\in {W}\right)\to \left({S}\in \left({J}{×}_{t}{K}\right)↔{S}\in \mathrm{topGen}\left(\mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\right)\right)$
4 1 txbasex ${⊢}\left({J}\in {V}\wedge {K}\in {W}\right)\to \mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\in \mathrm{V}$
5 eltg2b ${⊢}\mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\in \mathrm{V}\to \left({S}\in \mathrm{topGen}\left(\mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\right)↔\forall {p}\in {S}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\phantom{\rule{.4em}{0ex}}\left({p}\in {z}\wedge {z}\subseteq {S}\right)\right)$
6 4 5 syl ${⊢}\left({J}\in {V}\wedge {K}\in {W}\right)\to \left({S}\in \mathrm{topGen}\left(\mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\right)↔\forall {p}\in {S}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\phantom{\rule{.4em}{0ex}}\left({p}\in {z}\wedge {z}\subseteq {S}\right)\right)$
7 vex ${⊢}{x}\in \mathrm{V}$
8 vex ${⊢}{y}\in \mathrm{V}$
9 7 8 xpex ${⊢}{x}×{y}\in \mathrm{V}$
10 9 rgen2w ${⊢}\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{x}×{y}\in \mathrm{V}$
11 eqid ${⊢}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)=\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)$
12 eleq2 ${⊢}{z}={x}×{y}\to \left({p}\in {z}↔{p}\in \left({x}×{y}\right)\right)$
13 sseq1 ${⊢}{z}={x}×{y}\to \left({z}\subseteq {S}↔{x}×{y}\subseteq {S}\right)$
14 12 13 anbi12d ${⊢}{z}={x}×{y}\to \left(\left({p}\in {z}\wedge {z}\subseteq {S}\right)↔\left({p}\in \left({x}×{y}\right)\wedge {x}×{y}\subseteq {S}\right)\right)$
15 11 14 rexrnmpo ${⊢}\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{x}×{y}\in \mathrm{V}\to \left(\exists {z}\in \mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\phantom{\rule{.4em}{0ex}}\left({p}\in {z}\wedge {z}\subseteq {S}\right)↔\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({p}\in \left({x}×{y}\right)\wedge {x}×{y}\subseteq {S}\right)\right)$
16 10 15 ax-mp ${⊢}\exists {z}\in \mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\phantom{\rule{.4em}{0ex}}\left({p}\in {z}\wedge {z}\subseteq {S}\right)↔\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({p}\in \left({x}×{y}\right)\wedge {x}×{y}\subseteq {S}\right)$
17 16 ralbii ${⊢}\forall {p}\in {S}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\phantom{\rule{.4em}{0ex}}\left({p}\in {z}\wedge {z}\subseteq {S}\right)↔\forall {p}\in {S}\phantom{\rule{.4em}{0ex}}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({p}\in \left({x}×{y}\right)\wedge {x}×{y}\subseteq {S}\right)$
18 6 17 syl6bb ${⊢}\left({J}\in {V}\wedge {K}\in {W}\right)\to \left({S}\in \mathrm{topGen}\left(\mathrm{ran}\left({x}\in {J},{y}\in {K}⟼{x}×{y}\right)\right)↔\forall {p}\in {S}\phantom{\rule{.4em}{0ex}}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({p}\in \left({x}×{y}\right)\wedge {x}×{y}\subseteq {S}\right)\right)$
19 3 18 bitrd ${⊢}\left({J}\in {V}\wedge {K}\in {W}\right)\to \left({S}\in \left({J}{×}_{t}{K}\right)↔\forall {p}\in {S}\phantom{\rule{.4em}{0ex}}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {K}\phantom{\rule{.4em}{0ex}}\left({p}\in \left({x}×{y}\right)\wedge {x}×{y}\subseteq {S}\right)\right)$