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	$$⊢{\times }_s=\left(s\in \mathrm{V},t\in \mathrm{V}⟼𝛔\left(\mathrm{ran}\left(x\in s,y\in t⟼x\times y\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csx	$$class{\times }_s$$
1		vs	$$setvars$$
2		cvv	$$class\mathrm{V}$$
3		vt	$$setvart$$
4		csigagen	$$class𝛔$$
5		vx	$$setvarx$$
6	1	cv	$$setvars$$
7		vy	$$setvary$$
8	3	cv	$$setvart$$
9	5	cv	$$setvarx$$
10	7	cv	$$setvary$$
11	9 10	cxp	$$class\left(x\times y\right)$$
12	5 7 6 8 11	cmpo	$$class\left(x\in s,y\in t⟼x\times y\right)$$
13	12	crn	$$class\mathrm{ran}\left(x\in s,y\in t⟼x\times y\right)$$
14	13 4	cfv	$$class𝛔\left(\mathrm{ran}\left(x\in s,y\in t⟼x\times y\right)\right)$$
15	1 3 2 2 14	cmpo	$$class\left(s\in \mathrm{V},t\in \mathrm{V}⟼𝛔\left(\mathrm{ran}\left(x\in s,y\in t⟼x\times y\right)\right)\right)$$
16	0 15	wceq	$$wff{\times }_s=\left(s\in \mathrm{V},t\in \mathrm{V}⟼𝛔\left(\mathrm{ran}\left(x\in s,y\in t⟼x\times y\right)\right)\right)$$