# Metamath Proof Explorer

## Theorem sxuni

Description: The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017)

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

### Proof

Step Hyp Ref Expression
1 sxsigon ${⊢}\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 {S}×\bigcup {T}\right)$
2 issgon ${⊢}{S}{×}_{s}{T}\in \mathrm{sigAlgebra}\left(\bigcup {S}×\bigcup {T}\right)↔\left({S}{×}_{s}{T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup {S}×\bigcup {T}=\bigcup \left({S}{×}_{s}{T}\right)\right)$
3 2 simprbi ${⊢}{S}{×}_{s}{T}\in \mathrm{sigAlgebra}\left(\bigcup {S}×\bigcup {T}\right)\to \bigcup {S}×\bigcup {T}=\bigcup \left({S}{×}_{s}{T}\right)$
4 1 3 syl ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {T}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\right)\to \bigcup {S}×\bigcup {T}=\bigcup \left({S}{×}_{s}{T}\right)$