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 = s V , t V 𝛔 ran x s , y t x × y

Detailed syntax breakdown

Step Hyp Ref Expression
0 csx class × s
1 vs setvar s
2 cvv class V
3 vt setvar t
4 csigagen class 𝛔
5 vx setvar x
6 1 cv setvar s
7 vy setvar y
8 3 cv setvar t
9 5 cv setvar x
10 7 cv setvar y
11 9 10 cxp class x × y
12 5 7 6 8 11 cmpo class x s , y t x × y
13 12 crn class ran x s , y t x × y
14 13 4 cfv class 𝛔 ran x s , y t x × y
15 1 3 2 2 14 cmpo class s V , t V 𝛔 ran x s , y t x × y
16 0 15 wceq wff × s = s V , t V 𝛔 ran x s , y t x × y