Metamath Proof Explorer

Theorem elsx

Description: The cartesian product of two open sets is an element of the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017)

Ref Expression
Assertion elsx 
|- ( ( ( S e. V /\ T e. W ) /\ ( A e. S /\ B e. T ) ) -> ( A X. B ) e. ( S sX T ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran ( x e. S , y e. T |-> ( x X. y ) ) = ran ( x e. S , y e. T |-> ( x X. y ) )
2 1 txbasex 
 |-  ( ( S e. V /\ T e. W ) -> ran ( x e. S , y e. T |-> ( x X. y ) ) e. _V )
3 sssigagen 
 |-  ( ran ( x e. S , y e. T |-> ( x X. y ) ) e. _V -> ran ( x e. S , y e. T |-> ( x X. y ) ) C_ ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
4 2 3 syl 
 |-  ( ( S e. V /\ T e. W ) -> ran ( x e. S , y e. T |-> ( x X. y ) ) C_ ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
5 4 adantr 
 |-  ( ( ( S e. V /\ T e. W ) /\ ( A e. S /\ B e. T ) ) -> ran ( x e. S , y e. T |-> ( x X. y ) ) C_ ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
6 eqid 
 |-  ( A X. B ) = ( A X. B )
7 xpeq1 
 |-  ( x = A -> ( x X. y ) = ( A X. y ) )
8 7 eqeq2d 
 |-  ( x = A -> ( ( A X. B ) = ( x X. y ) <-> ( A X. B ) = ( A X. y ) ) )
9 xpeq2 
 |-  ( y = B -> ( A X. y ) = ( A X. B ) )
10 9 eqeq2d 
 |-  ( y = B -> ( ( A X. B ) = ( A X. y ) <-> ( A X. B ) = ( A X. B ) ) )
11 8 10 rspc2ev 
 |-  ( ( A e. S /\ B e. T /\ ( A X. B ) = ( A X. B ) ) -> E. x e. S E. y e. T ( A X. B ) = ( x X. y ) )
12 6 11 mp3an3 
 |-  ( ( A e. S /\ B e. T ) -> E. x e. S E. y e. T ( A X. B ) = ( x X. y ) )
13 xpexg 
 |-  ( ( A e. S /\ B e. T ) -> ( A X. B ) e. _V )
14 eqid 
 |-  ( x e. S , y e. T |-> ( x X. y ) ) = ( x e. S , y e. T |-> ( x X. y ) )
15 14 elrnmpog 
 |-  ( ( A X. B ) e. _V -> ( ( A X. B ) e. ran ( x e. S , y e. T |-> ( x X. y ) ) <-> E. x e. S E. y e. T ( A X. B ) = ( x X. y ) ) )
16 13 15 syl 
 |-  ( ( A e. S /\ B e. T ) -> ( ( A X. B ) e. ran ( x e. S , y e. T |-> ( x X. y ) ) <-> E. x e. S E. y e. T ( A X. B ) = ( x X. y ) ) )
17 12 16 mpbird 
 |-  ( ( A e. S /\ B e. T ) -> ( A X. B ) e. ran ( x e. S , y e. T |-> ( x X. y ) ) )
18 17 adantl 
 |-  ( ( ( S e. V /\ T e. W ) /\ ( A e. S /\ B e. T ) ) -> ( A X. B ) e. ran ( x e. S , y e. T |-> ( x X. y ) ) )
19 5 18 sseldd 
 |-  ( ( ( S e. V /\ T e. W ) /\ ( A e. S /\ B e. T ) ) -> ( A X. B ) e. ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
20 1 sxval 
 |-  ( ( S e. V /\ T e. W ) -> ( S sX T ) = ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
21 20 adantr 
 |-  ( ( ( S e. V /\ T e. W ) /\ ( A e. S /\ B e. T ) ) -> ( S sX T ) = ( sigaGen ` ran ( x e. S , y e. T |-> ( x X. y ) ) ) )
22 19 21 eleqtrrd 
 |-  ( ( ( S e. V /\ T e. W ) /\ ( A e. S /\ B e. T ) ) -> ( A X. B ) e. ( S sX T ) )