# Metamath Proof Explorer

## Theorem sxval

Description: Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017)

Ref Expression
Hypothesis sxval.1 ${⊢}{A}=\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)$
Assertion sxval ${⊢}\left({S}\in {V}\wedge {T}\in {W}\right)\to {S}{×}_{s}{T}=𝛔\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 sxval.1 ${⊢}{A}=\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)$
2 elex ${⊢}{S}\in {V}\to {S}\in \mathrm{V}$
3 elex ${⊢}{T}\in {W}\to {T}\in \mathrm{V}$
4 id ${⊢}{s}={S}\to {s}={S}$
5 eqidd ${⊢}{s}={S}\to {t}={t}$
6 eqidd ${⊢}{s}={S}\to {x}×{y}={x}×{y}$
7 4 5 6 mpoeq123dv ${⊢}{s}={S}\to \left({x}\in {s},{y}\in {t}⟼{x}×{y}\right)=\left({x}\in {S},{y}\in {t}⟼{x}×{y}\right)$
8 7 rneqd ${⊢}{s}={S}\to \mathrm{ran}\left({x}\in {s},{y}\in {t}⟼{x}×{y}\right)=\mathrm{ran}\left({x}\in {S},{y}\in {t}⟼{x}×{y}\right)$
9 8 fveq2d ${⊢}{s}={S}\to 𝛔\left(\mathrm{ran}\left({x}\in {s},{y}\in {t}⟼{x}×{y}\right)\right)=𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {t}⟼{x}×{y}\right)\right)$
10 eqidd ${⊢}{t}={T}\to {S}={S}$
11 id ${⊢}{t}={T}\to {t}={T}$
12 eqidd ${⊢}{t}={T}\to {x}×{y}={x}×{y}$
13 10 11 12 mpoeq123dv ${⊢}{t}={T}\to \left({x}\in {S},{y}\in {t}⟼{x}×{y}\right)=\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)$
14 13 rneqd ${⊢}{t}={T}\to \mathrm{ran}\left({x}\in {S},{y}\in {t}⟼{x}×{y}\right)=\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)$
15 14 fveq2d ${⊢}{t}={T}\to 𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {t}⟼{x}×{y}\right)\right)=𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
16 df-sx ${⊢}{×}_{s}=\left({s}\in \mathrm{V},{t}\in \mathrm{V}⟼𝛔\left(\mathrm{ran}\left({x}\in {s},{y}\in {t}⟼{x}×{y}\right)\right)\right)$
17 fvex ${⊢}𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)\in \mathrm{V}$
18 9 15 16 17 ovmpo ${⊢}\left({S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\to {S}{×}_{s}{T}=𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
19 2 3 18 syl2an ${⊢}\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)$
20 1 fveq2i ${⊢}𝛔\left({A}\right)=𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
21 19 20 eqtr4di ${⊢}\left({S}\in {V}\wedge {T}\in {W}\right)\to {S}{×}_{s}{T}=𝛔\left({A}\right)$