Metamath Proof Explorer

Theorem sxbrsiga

Description: The product sigma-algebra ( BrSiga sX BrSiga ) is the Borel algebra on ( RR X. RR ) See example 5.1.1 of Cohn p. 143 . (Contributed by Thierry Arnoux, 10-Oct-2017)

Ref Expression
Hypothesis sxbrsiga.0 
|- J = ( topGen ` ran (,) )
Assertion sxbrsiga 
|- ( BrSiga sX BrSiga ) = ( sigaGen ` ( J tX J ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 
 |-  J = ( topGen ` ran (,) )
2 brsigarn 
 |-  BrSiga e. ( sigAlgebra ` RR )
3 eqid 
 |-  ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) )
4 3 sxval 
 |-  ( ( BrSiga e. ( sigAlgebra ` RR ) /\ BrSiga e. ( sigAlgebra ` RR ) ) -> ( BrSiga sX BrSiga ) = ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) ) )
5 2 2 4 mp2an 
 |-  ( BrSiga sX BrSiga ) = ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) )
6 br2base 
 |-  U. ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = ( RR X. RR )
7 1 tpr2uni 
 |-  U. ( J tX J ) = ( RR X. RR )
8 6 7 eqtr4i 
 |-  U. ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = U. ( J tX J )
9 brsigasspwrn 
 |-  BrSiga C_ ~P RR
10 9 sseli 
 |-  ( e e. BrSiga -> e e. ~P RR )
11 10 elpwid 
 |-  ( e e. BrSiga -> e C_ RR )
12 9 sseli 
 |-  ( f e. BrSiga -> f e. ~P RR )
13 12 elpwid 
 |-  ( f e. BrSiga -> f C_ RR )
14 xpinpreima2 
 |-  ( ( e C_ RR /\ f C_ RR ) -> ( e X. f ) = ( ( `' ( 1st |` ( RR X. RR ) ) " e ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " f ) ) )
15 11 13 14 syl2an 
 |-  ( ( e e. BrSiga /\ f e. BrSiga ) -> ( e X. f ) = ( ( `' ( 1st |` ( RR X. RR ) ) " e ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " f ) ) )
16 1 tpr2tp 
 |-  ( J tX J ) e. ( TopOn ` ( RR X. RR ) )
17 sigagensiga 
 |-  ( ( J tX J ) e. ( TopOn ` ( RR X. RR ) ) -> ( sigaGen ` ( J tX J ) ) e. ( sigAlgebra ` U. ( J tX J ) ) )
18 16 17 ax-mp 
 |-  ( sigaGen ` ( J tX J ) ) e. ( sigAlgebra ` U. ( J tX J ) )
19 elrnsiga 
 |-  ( ( sigaGen ` ( J tX J ) ) e. ( sigAlgebra ` U. ( J tX J ) ) -> ( sigaGen ` ( J tX J ) ) e. U. ran sigAlgebra )
20 18 19 mp1i 
 |-  ( ( e e. BrSiga /\ f e. BrSiga ) -> ( sigaGen ` ( J tX J ) ) e. U. ran sigAlgebra )
21 16 a1i 
 |-  ( e e. BrSiga -> ( J tX J ) e. ( TopOn ` ( RR X. RR ) ) )
22 21 sgsiga 
 |-  ( e e. BrSiga -> ( sigaGen ` ( J tX J ) ) e. U. ran sigAlgebra )
23 elrnsiga 
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
24 2 23 mp1i 
 |-  ( e e. BrSiga -> BrSiga e. U. ran sigAlgebra )
25 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
26 1 25 eqeltri 
 |-  J e. ( TopOn ` RR )
27 tx1cn 
 |-  ( ( J e. ( TopOn ` RR ) /\ J e. ( TopOn ` RR ) ) -> ( 1st |` ( RR X. RR ) ) e. ( ( J tX J ) Cn J ) )
28 26 26 27 mp2an 
 |-  ( 1st |` ( RR X. RR ) ) e. ( ( J tX J ) Cn J )
29 28 a1i 
 |-  ( e e. BrSiga -> ( 1st |` ( RR X. RR ) ) e. ( ( J tX J ) Cn J ) )
30 eqidd 
 |-  ( e e. BrSiga -> ( sigaGen ` ( J tX J ) ) = ( sigaGen ` ( J tX J ) ) )
31 df-brsiga 
 |-  BrSiga = ( sigaGen ` ( topGen ` ran (,) ) )
32 1 fveq2i 
 |-  ( sigaGen ` J ) = ( sigaGen ` ( topGen ` ran (,) ) )
33 31 32 eqtr4i 
 |-  BrSiga = ( sigaGen ` J )
34 33 a1i 
 |-  ( e e. BrSiga -> BrSiga = ( sigaGen ` J ) )
35 29 30 34 cnmbfm 
 |-  ( e e. BrSiga -> ( 1st |` ( RR X. RR ) ) e. ( ( sigaGen ` ( J tX J ) ) MblFnM BrSiga ) )
36 id 
 |-  ( e e. BrSiga -> e e. BrSiga )
37 22 24 35 36 mbfmcnvima 
 |-  ( e e. BrSiga -> ( `' ( 1st |` ( RR X. RR ) ) " e ) e. ( sigaGen ` ( J tX J ) ) )
38 37 adantr 
 |-  ( ( e e. BrSiga /\ f e. BrSiga ) -> ( `' ( 1st |` ( RR X. RR ) ) " e ) e. ( sigaGen ` ( J tX J ) ) )
39 16 a1i 
 |-  ( f e. BrSiga -> ( J tX J ) e. ( TopOn ` ( RR X. RR ) ) )
40 39 sgsiga 
 |-  ( f e. BrSiga -> ( sigaGen ` ( J tX J ) ) e. U. ran sigAlgebra )
41 2 23 mp1i 
 |-  ( f e. BrSiga -> BrSiga e. U. ran sigAlgebra )
42 tx2cn 
 |-  ( ( J e. ( TopOn ` RR ) /\ J e. ( TopOn ` RR ) ) -> ( 2nd |` ( RR X. RR ) ) e. ( ( J tX J ) Cn J ) )
43 26 26 42 mp2an 
 |-  ( 2nd |` ( RR X. RR ) ) e. ( ( J tX J ) Cn J )
44 43 a1i 
 |-  ( f e. BrSiga -> ( 2nd |` ( RR X. RR ) ) e. ( ( J tX J ) Cn J ) )
45 eqidd 
 |-  ( f e. BrSiga -> ( sigaGen ` ( J tX J ) ) = ( sigaGen ` ( J tX J ) ) )
46 33 a1i 
 |-  ( f e. BrSiga -> BrSiga = ( sigaGen ` J ) )
47 44 45 46 cnmbfm 
 |-  ( f e. BrSiga -> ( 2nd |` ( RR X. RR ) ) e. ( ( sigaGen ` ( J tX J ) ) MblFnM BrSiga ) )
48 id 
 |-  ( f e. BrSiga -> f e. BrSiga )
49 40 41 47 48 mbfmcnvima 
 |-  ( f e. BrSiga -> ( `' ( 2nd |` ( RR X. RR ) ) " f ) e. ( sigaGen ` ( J tX J ) ) )
50 49 adantl 
 |-  ( ( e e. BrSiga /\ f e. BrSiga ) -> ( `' ( 2nd |` ( RR X. RR ) ) " f ) e. ( sigaGen ` ( J tX J ) ) )
51 inelsiga 
 |-  ( ( ( sigaGen ` ( J tX J ) ) e. U. ran sigAlgebra /\ ( `' ( 1st |` ( RR X. RR ) ) " e ) e. ( sigaGen ` ( J tX J ) ) /\ ( `' ( 2nd |` ( RR X. RR ) ) " f ) e. ( sigaGen ` ( J tX J ) ) ) -> ( ( `' ( 1st |` ( RR X. RR ) ) " e ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " f ) ) e. ( sigaGen ` ( J tX J ) ) )
52 20 38 50 51 syl3anc 
 |-  ( ( e e. BrSiga /\ f e. BrSiga ) -> ( ( `' ( 1st |` ( RR X. RR ) ) " e ) i^i ( `' ( 2nd |` ( RR X. RR ) ) " f ) ) e. ( sigaGen ` ( J tX J ) ) )
53 15 52 eqeltrd 
 |-  ( ( e e. BrSiga /\ f e. BrSiga ) -> ( e X. f ) e. ( sigaGen ` ( J tX J ) ) )
54 53 rgen2 
 |-  A. e e. BrSiga A. f e. BrSiga ( e X. f ) e. ( sigaGen ` ( J tX J ) )
55 eqid 
 |-  ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) )
56 55 rnmposs 
 |-  ( A. e e. BrSiga A. f e. BrSiga ( e X. f ) e. ( sigaGen ` ( J tX J ) ) -> ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) C_ ( sigaGen ` ( J tX J ) ) )
57 54 56 ax-mp 
 |-  ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) C_ ( sigaGen ` ( J tX J ) )
58 sigagenss2 
 |-  ( ( U. ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) = U. ( J tX J ) /\ ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) C_ ( sigaGen ` ( J tX J ) ) /\ ( J tX J ) e. ( TopOn ` ( RR X. RR ) ) ) -> ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) ) C_ ( sigaGen ` ( J tX J ) ) )
59 8 57 16 58 mp3an 
 |-  ( sigaGen ` ran ( e e. BrSiga , f e. BrSiga |-> ( e X. f ) ) ) C_ ( sigaGen ` ( J tX J ) )
60 5 59 eqsstri 
 |-  ( BrSiga sX BrSiga ) C_ ( sigaGen ` ( J tX J ) )
61 1 sxbrsigalem6 
 |-  ( sigaGen ` ( J tX J ) ) C_ ( BrSiga sX BrSiga )
62 60 61 eqssi 
 |-  ( BrSiga sX BrSiga ) = ( sigaGen ` ( J tX J ) )