Theorem sxsigon

Description: A product sigma-algebra is a sigma-algebra on the product of the bases. (Contributed by Thierry Arnoux, 1-Jun-2017)

	Ref	Expression
Assertion	sxsigon	|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) e. ( sigAlgebra ` ( U. S X. U. T ) ) )

Proof

Step	Hyp	Ref	Expression
1		sxsiga	|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) e. U. ran sigAlgebra )
2		eqid	|- ran ( x e. S , y e. T |-> ( x X. y ) ) = ran ( x e. S , y e. T |-> ( x X. y ) )
3		eqid	|- U. S = U. S
4		eqid	|- U. T = U. T
5	2 3 4	txuni2	|- ( U. S X. U. T ) = U. ran ( x e. S , y e. T |-> ( x X. y ) )
6	2	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 ) ) ) )
7	6	unieqd	|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> U. ( S sX T ) = U. ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
8		mpoexga	|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( x e. S , y e. T |-> ( x X. y ) ) e. _V )
9		rnexg	|- ( ( x e. S , y e. T |-> ( x X. y ) ) e. _V -> ran ( x e. S , y e. T |-> ( x X. y ) ) e. _V )
10		unisg	|- ( ran ( x e. S , y e. T |-> ( x X. y ) ) e. _V -> U. ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) = U. ran ( x e. S , y e. T |-> ( x X. y ) ) )
11	8 9 10	3syl	|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> U. ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) = U. ran ( x e. S , y e. T |-> ( x X. y ) ) )
12	7 11	eqtrd	|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> U. ( S sX T ) = U. ran ( x e. S , y e. T |-> ( x X. y ) ) )
13	5 12	eqtr4id	|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( U. S X. U. T ) = U. ( S sX T ) )
14		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 ) ) )
15	1 13 14	sylanbrc	|- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) e. ( sigAlgebra ` ( U. S X. U. T ) ) )