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
|- sX = ( s e. _V , t e. _V |-> ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csx
 |-  sX
1 vs
 |-  s
2 cvv
 |-  _V
3 vt
 |-  t
4 csigagen
 |-  sigaGen
5 vx
 |-  x
6 1 cv
 |-  s
7 vy
 |-  y
8 3 cv
 |-  t
9 5 cv
 |-  x
10 7 cv
 |-  y
11 9 10 cxp
 |-  ( x X. y )
12 5 7 6 8 11 cmpo
 |-  ( x e. s , y e. t |-> ( x X. y ) )
13 12 crn
 |-  ran ( x e. s , y e. t |-> ( x X. y ) )
14 13 4 cfv
 |-  ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) )
15 1 3 2 2 14 cmpo
 |-  ( s e. _V , t e. _V |-> ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) )
16 0 15 wceq
 |-  sX = ( s e. _V , t e. _V |-> ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) )