Metamath Proof Explorer


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 ‘ ( 𝑆 × 𝑇 ) ) )