# Metamath Proof Explorer

## Theorem sxsiga

Description: A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017)

Ref Expression
Assertion sxsiga ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {S}{×}_{s}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$

### 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 sxval ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {S}{×}_{s}{T}=𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
3 1 txbasex ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\in \mathrm{V}$
4 sigagensiga ${⊢}\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\in \mathrm{V}\to 𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)\in \mathrm{sigAlgebra}\left(\bigcup \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
5 3 4 syl ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to 𝛔\left(\mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)\in \mathrm{sigAlgebra}\left(\bigcup \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
6 2 5 eqeltrd ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {S}{×}_{s}{T}\in \mathrm{sigAlgebra}\left(\bigcup \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)$
7 elrnsiga ${⊢}{S}{×}_{s}{T}\in \mathrm{sigAlgebra}\left(\bigcup \mathrm{ran}\left({x}\in {S},{y}\in {T}⟼{x}×{y}\right)\right)\to {S}{×}_{s}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
8 6 7 syl ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to {S}{×}_{s}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$