Definition df-sx 32136

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

Assertion

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

Distinct variable group:   𝑡,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-sx

Step	Hyp	Ref	Expression
1		csx 32135	. 2 class ×s
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cvv 3430	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1540	. . . . . 6 class 𝑠
8	3	cv 1540	. . . . . 6 class 𝑡
9	5	cv 1540	. . . . . . 7 class 𝑥
10	6	cv 1540	. . . . . . 7 class 𝑦
11	9, 10	cxp 5586	. . . . . 6 class (𝑥 × 𝑦)
12	5, 6, 7, 8, 11	cmpo 7270	. . . . 5 class (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦))
13	12	crn 5589	. . . 4 class ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦))
14		csigagen 32085	. . . 4 class sigaGen
15	13, 14	cfv 6430	. . 3 class (sigaGen‘ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦)))
16	2, 3, 4, 4, 15	cmpo 7270	. 2 class (𝑠 ∈ V, 𝑡 ∈ V ↦ (sigaGen‘ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦))))
17	1, 16	wceq 1541	1 wff ×s = (𝑠 ∈ V, 𝑡 ∈ V ↦ (sigaGen‘ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦))))

This definition is referenced by:  sxval  32137