Metamath Proof Explorer

Theorem sxval

Description: Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017)

Ref Expression
Hypothesis sxval.1 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) )
Assertion sxval ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sxval.1 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) )
2 elex ⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
3 elex ⊢ ( 𝑇 ∈ 𝑊 → 𝑇 ∈ V )
4 id ⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 )
5 eqidd ⊢ ( 𝑠 = 𝑆 → 𝑡 = 𝑡 )
6 eqidd ⊢ ( 𝑠 = 𝑆 → ( 𝑥 × 𝑦 ) = ( 𝑥 × 𝑦 ) )
7 4 5 6 mpoeq123dv ⊢ ( 𝑠 = 𝑆 → ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) )
8 7 rneqd ⊢ ( 𝑠 = 𝑆 → ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) )
9 8 fveq2d ⊢ ( 𝑠 = 𝑆 → ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) )
10 eqidd ⊢ ( 𝑡 = 𝑇 → 𝑆 = 𝑆 )
11 id ⊢ ( 𝑡 = 𝑇 → 𝑡 = 𝑇 )
12 eqidd ⊢ ( 𝑡 = 𝑇 → ( 𝑥 × 𝑦 ) = ( 𝑥 × 𝑦 ) )
13 10 11 12 mpoeq123dv ⊢ ( 𝑡 = 𝑇 → ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) )
14 13 rneqd ⊢ ( 𝑡 = 𝑇 → ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) )
15 14 fveq2d ⊢ ( 𝑡 = 𝑇 → ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
16 df-sx ⊢ ×s = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) )
17 fvex ⊢ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) ∈ V
18 9 15 16 17 ovmpo ⊢ ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
19 2 3 18 syl2an ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) ) )
20 1 fveq2i ⊢ ( sigaGen ‘ 𝐴 ) = ( sigaGen ‘ ran ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑇 ↦ ( 𝑥 × 𝑦 ) ) )
21 19 20 eqtr4di ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ( 𝑆 ×s 𝑇 ) = ( sigaGen ‘ 𝐴 ) )