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	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) ∈ ( sigAlgebra ‘ ( ∪ 𝑆 × ∪ 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sxsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) ∈ ∪ ran sigAlgebra )
2		eqid	⊢ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) )
3		eqid	⊢ ∪ 𝑆 = ∪ 𝑆
4		eqid	⊢ ∪ 𝑇 = ∪ 𝑇
5	2 3 4	txuni2	⊢ ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) )
6	2	sxval	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
7	6	unieqd	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ∪ ( 𝑆 ×s 𝑇 ) = ∪ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
8		mpoexga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V )
9		rnexg	⊢ ( ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V → ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V )
10		unisg	⊢ ( ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V → ∪ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) = ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) )
11	8 9 10	3syl	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ∪ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) = ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) )
12	7 11	eqtrd	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ∪ ( 𝑆 ×s 𝑇 ) = ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) )
13	5 12	eqtr4id	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×s 𝑇 ) )
14		issgon	⊢ ( ( 𝑆 ×s 𝑇 ) ∈ ( sigAlgebra ‘ ( ∪ 𝑆 × ∪ 𝑇 ) ) ↔ ( ( 𝑆 ×s 𝑇 ) ∈ ∪ ran sigAlgebra ∧ ( ∪ 𝑆 × ∪ 𝑇 ) = ∪ ( 𝑆 ×s 𝑇 ) ) )
15	1 13 14	sylanbrc	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) ∈ ( sigAlgebra ‘ ( ∪ 𝑆 × ∪ 𝑇 ) ) )