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 = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csx	⊢ ×s
1		vs	⊢ 𝑠
2		cvv	⊢ V
3		vt	⊢ 𝑡
4		csigagen	⊢ sigaGen
5		vx	⊢ 𝑥
6	1	cv	⊢ 𝑠
7		vy	⊢ 𝑦
8	3	cv	⊢ 𝑡
9	5	cv	⊢ 𝑥
10	7	cv	⊢ 𝑦
11	9 10	cxp	⊢ ( 𝑥 × 𝑦 )
12	5 7 6 8 11	cmpo	⊢ ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) )
13	12	crn	⊢ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) )
14	13 4	cfv	⊢ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) )
15	1 3 2 2 14	cmpo	⊢ ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) )
16	0 15	wceq	⊢ ×s = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( sigaGen ‘ ran ( 𝑥 ∈ 𝑠 , 𝑦 ∈ 𝑡 ↦ ( 𝑥 × 𝑦 ) ) ) )