Metamath Proof Explorer


Theorem sxval

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

Ref Expression
Hypothesis sxval.1 A = ran x S , y T x × y
Assertion sxval S V T W S × s T = 𝛔 A

Proof

Step Hyp Ref Expression
1 sxval.1 A = ran x S , y T x × y
2 elex S V S V
3 elex T W T V
4 id s = S s = S
5 eqidd s = S t = t
6 eqidd s = S x × y = x × y
7 4 5 6 mpoeq123dv s = S x s , y t x × y = x S , y t x × y
8 7 rneqd s = S ran x s , y t x × y = ran x S , y t x × y
9 8 fveq2d s = S 𝛔 ran x s , y t x × y = 𝛔 ran x S , y t x × y
10 eqidd t = T S = S
11 id t = T t = T
12 eqidd t = T x × y = x × y
13 10 11 12 mpoeq123dv t = T x S , y t x × y = x S , y T x × y
14 13 rneqd t = T ran x S , y t x × y = ran x S , y T x × y
15 14 fveq2d t = T 𝛔 ran x S , y t x × y = 𝛔 ran x S , y T x × y
16 df-sx × s = s V , t V 𝛔 ran x s , y t x × y
17 fvex 𝛔 ran x S , y T x × y V
18 9 15 16 17 ovmpo S V T V S × s T = 𝛔 ran x S , y T x × y
19 2 3 18 syl2an S V T W S × s T = 𝛔 ran x S , y T x × y
20 1 fveq2i 𝛔 A = 𝛔 ran x S , y T x × y
21 19 20 eqtr4di S V T W S × s T = 𝛔 A