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 e. S , y e. T |-> ( x X. y ) )
Assertion sxval 
|- ( ( S e. V /\ T e. W ) -> ( S sX T ) = ( sigaGen ` A ) )

Proof

Step Hyp Ref Expression
1 sxval.1 
 |-  A = ran ( x e. S , y e. T |-> ( x X. y ) )
2 elex 
 |-  ( S e. V -> S e. _V )
3 elex 
 |-  ( T e. W -> T e. _V )
4 id 
 |-  ( s = S -> s = S )
5 eqidd 
 |-  ( s = S -> t = t )
6 eqidd 
 |-  ( s = S -> ( x X. y ) = ( x X. y ) )
7 4 5 6 mpoeq123dv 
 |-  ( s = S -> ( x e. s , y e. t |-> ( x X. y ) ) = ( x e. S , y e. t |-> ( x X. y ) ) )
8 7 rneqd 
 |-  ( s = S -> ran ( x e. s , y e. t |-> ( x X. y ) ) = ran ( x e. S , y e. t |-> ( x X. y ) ) )
9 8 fveq2d 
 |-  ( s = S -> ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) = ( sigaGen ` ran ( x e. S , y e. t |-> ( x X. y ) ) ) )
10 eqidd 
 |-  ( t = T -> S = S )
11 id 
 |-  ( t = T -> t = T )
12 eqidd 
 |-  ( t = T -> ( x X. y ) = ( x X. y ) )
13 10 11 12 mpoeq123dv 
 |-  ( t = T -> ( x e. S , y e. t |-> ( x X. y ) ) = ( x e. S , y e. T |-> ( x X. y ) ) )
14 13 rneqd 
 |-  ( t = T -> ran ( x e. S , y e. t |-> ( x X. y ) ) = ran ( x e. S , y e. T |-> ( x X. y ) ) )
15 14 fveq2d 
 |-  ( t = T -> ( sigaGen ` ran ( x e. S , y e. t |-> ( x X. y ) ) ) = ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
16 df-sx 
 |-  sX = ( s e. _V , t e. _V |-> ( sigaGen ` ran ( x e. s , y e. t |-> ( x X. y ) ) ) )
17 fvex 
 |-  ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) e. _V
18 9 15 16 17 ovmpo 
 |-  ( ( S e. _V /\ T e. _V ) -> ( S sX T ) = ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
19 2 3 18 syl2an 
 |-  ( ( S e. V /\ T e. W ) -> ( S sX T ) = ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
20 1 fveq2i 
 |-  ( sigaGen ` A ) = ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) )
21 19 20 eqtr4di 
 |-  ( ( S e. V /\ T e. W ) -> ( S sX T ) = ( sigaGen ` A ) )