# Metamath Proof Explorer

## Theorem elsx

Description: The cartesian product of two open sets is an element of the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017)

Ref Expression
Assertion elsx ${⊢}\left(\left({S}\in {V}\wedge {T}\in {W}\right)\wedge \left({A}\in {S}\wedge {B}\in {T}\right)\right)\to {A}×{B}\in \left({S}{×}_{s}{T}\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)=\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)$
2 1 txbasex ${⊢}\left({S}\in {V}\wedge {T}\in {W}\right)\to \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\in \mathrm{V}$
3 sssigagen ${⊢}\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\in \mathrm{V}\to \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\subseteq 𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
4 2 3 syl ${⊢}\left({S}\in {V}\wedge {T}\in {W}\right)\to \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\subseteq 𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
5 4 adantr ${⊢}\left(\left({S}\in {V}\wedge {T}\in {W}\right)\wedge \left({A}\in {S}\wedge {B}\in {T}\right)\right)\to \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\subseteq 𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
6 eqid ${⊢}{A}×{B}={A}×{B}$
7 xpeq1 ${⊢}{x}={A}\to {x}×{y}={A}×{y}$
8 7 eqeq2d ${⊢}{x}={A}\to \left({A}×{B}={x}×{y}↔{A}×{B}={A}×{y}\right)$
9 xpeq2 ${⊢}{y}={B}\to {A}×{y}={A}×{B}$
10 9 eqeq2d ${⊢}{y}={B}\to \left({A}×{B}={A}×{y}↔{A}×{B}={A}×{B}\right)$
11 8 10 rspc2ev ${⊢}\left({A}\in {S}\wedge {B}\in {T}\wedge {A}×{B}={A}×{B}\right)\to \exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {y}\in {T}\phantom{\rule{.4em}{0ex}}{A}×{B}={x}×{y}$
12 6 11 mp3an3 ${⊢}\left({A}\in {S}\wedge {B}\in {T}\right)\to \exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {y}\in {T}\phantom{\rule{.4em}{0ex}}{A}×{B}={x}×{y}$
13 xpexg ${⊢}\left({A}\in {S}\wedge {B}\in {T}\right)\to {A}×{B}\in \mathrm{V}$
14 eqid ${⊢}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)=\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)$
15 14 elrnmpog ${⊢}{A}×{B}\in \mathrm{V}\to \left({A}×{B}\in \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {y}\in {T}\phantom{\rule{.4em}{0ex}}{A}×{B}={x}×{y}\right)$
16 13 15 syl ${⊢}\left({A}\in {S}\wedge {B}\in {T}\right)\to \left({A}×{B}\in \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {y}\in {T}\phantom{\rule{.4em}{0ex}}{A}×{B}={x}×{y}\right)$
17 12 16 mpbird ${⊢}\left({A}\in {S}\wedge {B}\in {T}\right)\to {A}×{B}\in \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)$
18 17 adantl ${⊢}\left(\left({S}\in {V}\wedge {T}\in {W}\right)\wedge \left({A}\in {S}\wedge {B}\in {T}\right)\right)\to {A}×{B}\in \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)$
19 5 18 sseldd ${⊢}\left(\left({S}\in {V}\wedge {T}\in {W}\right)\wedge \left({A}\in {S}\wedge {B}\in {T}\right)\right)\to {A}×{B}\in 𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
20 1 sxval ${⊢}\left({S}\in {V}\wedge {T}\in {W}\right)\to {S}{×}_{s}{T}=𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
21 20 adantr ${⊢}\left(\left({S}\in {V}\wedge {T}\in {W}\right)\wedge \left({A}\in {S}\wedge {B}\in {T}\right)\right)\to {S}{×}_{s}{T}=𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
22 19 21 eleqtrrd ${⊢}\left(\left({S}\in {V}\wedge {T}\in {W}\right)\wedge \left({A}\in {S}\wedge {B}\in {T}\right)\right)\to {A}×{B}\in \left({S}{×}_{s}{T}\right)$