Definition df-sx 30252

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

Assertion

Ref	Expression
df-sx	|- ×s = ( s e. _V , t e. _V |-> (sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) )

Distinct variable group:   t, s, x, y

Detailed syntax breakdown of Definition df-sx

Step	Hyp	Ref	Expression
1		csx 30251	. 2 class ×s
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cvv 3200	. . 3 class _V
5		vx	. . . . . 6 setvar x
6		vy	. . . . . 6 setvar y
7	2	cv 1482	. . . . . 6 class s
8	3	cv 1482	. . . . . 6 class t
9	5	cv 1482	. . . . . . 7 class x
10	6	cv 1482	. . . . . . 7 class y
11	9, 10	cxp 5112	. . . . . 6 class ( x X. y )
12	5, 6, 7, 8, 11	cmpt2 6652	. . . . 5 class ( x e. s , y e. t |-> ( x X. y ) )
13	12	crn 5115	. . . 4 class ran ( x e. s , y e. t |-> ( x X. y ) )
14		csigagen 30201	. . . 4 class sigaGen
15	13, 14	cfv 5888	. . 3 class (sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) )
16	2, 3, 4, 4, 15	cmpt2 6652	. 2 class ( s e. _V , t e. _V |-> (sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) )
17	1, 16	wceq 1483	1 wff ×s = ( s e. _V , t e. _V |-> (sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) )

This definition is referenced by:  sxval  30253