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 e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( U. S X. U. T ) = U. ( S sX T ) )

Proof

Step Hyp Ref Expression
1 sxsigon 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) e. ( sigAlgebra ` ( U. S X. U. T ) ) )
2 issgon 
 |-  ( ( S sX T ) e. ( sigAlgebra ` ( U. S X. U. T ) ) <-> ( ( S sX T ) e. U. ran sigAlgebra /\ ( U. S X. U. T ) = U. ( S sX T ) ) )
3 2 simprbi 
 |-  ( ( S sX T ) e. ( sigAlgebra ` ( U. S X. U. T ) ) -> ( U. S X. U. T ) = U. ( S sX T ) )
4 1 3 syl 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( U. S X. U. T ) = U. ( S sX T ) )