Metamath Proof Explorer


Definition df-sx

Description: Define the product sigma-algebra operation, analogous to df-tx . (Contributed by Thierry Arnoux, 1-Jun-2017)

Ref Expression
Assertion df-sx ×s = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥𝑠 , 𝑦𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csx ×s
1 vs 𝑠
2 cvv V
3 vt 𝑡
4 csigagen sigaGen
5 vx 𝑥
6 1 cv 𝑠
7 vy 𝑦
8 3 cv 𝑡
9 5 cv 𝑥
10 7 cv 𝑦
11 9 10 cxp ( 𝑥 × 𝑦 )
12 5 7 6 8 11 cmpo ( 𝑥𝑠 , 𝑦𝑡 ↦ ( 𝑥 × 𝑦 ) )
13 12 crn ran ( 𝑥𝑠 , 𝑦𝑡 ↦ ( 𝑥 × 𝑦 ) )
14 13 4 cfv ( sigaGen ‘ ran ( 𝑥𝑠 , 𝑦𝑡 ↦ ( 𝑥 × 𝑦 ) ) )
15 1 3 2 2 14 cmpo ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥𝑠 , 𝑦𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) )
16 0 15 wceq ×s = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥𝑠 , 𝑦𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) )