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 S ran sigAlgebra T ran sigAlgebra S × T = S × s T

Proof

Step Hyp Ref Expression
1 sxsigon S ran sigAlgebra T ran sigAlgebra S × s T sigAlgebra S × T
2 issgon S × s T sigAlgebra S × T S × s T ran sigAlgebra S × T = S × s T
3 2 simprbi S × s T sigAlgebra S × T S × T = S × s T
4 1 3 syl S ran sigAlgebra T ran sigAlgebra S × T = S × s T