Theorem sxsiga

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

	Ref	Expression
Assertion	sxsiga	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) ∈ ∪ ran sigAlgebra )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) )
2	1	sxval	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
3	1	txbasex	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V )
4		sigagensiga	⊢ ( ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ∈ V → ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) ∈ ( sigAlgebra ‘ ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
5	3 4	syl	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) ∈ ( sigAlgebra ‘ ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
6	2 5	eqeltrd	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) ∈ ( sigAlgebra ‘ ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
7		elrnsiga	⊢ ( ( 𝑆 ×s 𝑇 ) ∈ ( sigAlgebra ‘ ∪ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) → ( 𝑆 ×s 𝑇 ) ∈ ∪ ran sigAlgebra )
8	6 7	syl	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra ) → ( 𝑆 ×s 𝑇 ) ∈ ∪ ran sigAlgebra )