sxval

Description: Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017)

		Ref	Expression
	Hypothesis	sxval.1	$⊢ A = ran (x \in S, y \in T ⟼ x \times y)$
	Assertion	sxval	$⊢ (S \in V \land T \in W) \to S \times_{s} T = 𝛔 (A)$

Step	Hyp	Ref	Expression
1		sxval.1	$⊢ A = ran (x \in S, y \in T ⟼ x \times y)$
2		elex	$⊢ S \in V \to S \in V$
3		elex	$⊢ T \in W \to T \in V$
4		id	$⊢ s = S \to s = S$
5		eqidd	$⊢ s = S \to t = t$
6		eqidd	$⊢ s = S \to x \times y = x \times y$
7	4 5 6	mpoeq123dv	$⊢ s = S \to (x \in s, y \in t ⟼ x \times y) = (x \in S, y \in t ⟼ x \times y)$
8	7	rneqd	$⊢ s = S \to ran (x \in s, y \in t ⟼ x \times y) = ran (x \in S, y \in t ⟼ x \times y)$
9	8	fveq2d	$⊢ s = S \to 𝛔 (ran (x \in s, y \in t ⟼ x \times y)) = 𝛔 (ran (x \in S, y \in t ⟼ x \times y))$
10		eqidd	$⊢ t = T \to S = S$
11		id	$⊢ t = T \to t = T$
12		eqidd	$⊢ t = T \to x \times y = x \times y$
13	10 11 12	mpoeq123dv	$⊢ t = T \to (x \in S, y \in t ⟼ x \times y) = (x \in S, y \in T ⟼ x \times y)$
14	13	rneqd	$⊢ t = T \to ran (x \in S, y \in t ⟼ x \times y) = ran (x \in S, y \in T ⟼ x \times y)$
15	14	fveq2d	$⊢ t = T \to 𝛔 (ran (x \in S, y \in t ⟼ x \times y)) = 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
16		df-sx	$⊢ \times_{s} = (s \in V, t \in V ⟼ 𝛔 (ran (x \in s, y \in t ⟼ x \times y)))$
17		fvex	$⊢ 𝛔 (ran (x \in S, y \in T ⟼ x \times y)) \in V$
18	9 15 16 17	ovmpo	$⊢ (S \in V \land T \in V) \to S \times_{s} T = 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
19	2 3 18	syl2an	$⊢ (S \in V \land T \in W) \to S \times_{s} T = 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
20	1	fveq2i	$⊢ 𝛔 (A) = 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
21	19 20	eqtr4di	$⊢ (S \in V \land T \in W) \to S \times_{s} T = 𝛔 (A)$

Metamath Proof Explorer