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\times \bigcup T=\bigcup \left(S{\times }_{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{\times }_{s}T\in \mathrm{sigAlgebra}\left(\bigcup S\times \bigcup T\right)$$
2		issgon	$$⊢S{\times }_{s}T\in \mathrm{sigAlgebra}\left(\bigcup S\times \bigcup T\right)\leftrightarrow \left(S{\times }_{s}T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \bigcup S\times \bigcup T=\bigcup \left(S{\times }_{s}T\right)\right)$$
3	2	simprbi	$$⊢S{\times }_{s}T\in \mathrm{sigAlgebra}\left(\bigcup S\times \bigcup T\right)\to \bigcup S\times \bigcup T=\bigcup \left(S{\times }_{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\times \bigcup T=\bigcup \left(S{\times }_{s}T\right)$$