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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran ( x e. S , y e. T |-> ( x X. y ) ) = ran ( x e. S , y e. T |-> ( x X. y ) )
2 1 sxval 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) = ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
3 1 txbasex 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ran ( x e. S , y e. T |-> ( x X. y ) ) e. _V )
4 sigagensiga 
 |-  ( ran ( x e. S , y e. T |-> ( x X. y ) ) e. _V -> ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) e. ( sigAlgebra ` U. ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
5 3 4 syl 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) e. ( sigAlgebra ` U. ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
6 2 5 eqeltrd 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) e. ( sigAlgebra ` U. ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
7 elrnsiga 
 |-  ( ( S sX T ) e. ( sigAlgebra ` U. ran ( x e. S , y e. T |-> ( x X. y ) ) ) -> ( S sX T ) e. U. ran sigAlgebra )
8 6 7 syl 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) e. U. ran sigAlgebra )