Metamath Proof Explorer

Theorem br2base

Description: The base set for the generator of the Borel sigma-algebra on ( RR X. RR ) is indeed ( RR X. RR ) . (Contributed by Thierry Arnoux, 22-Sep-2017)

Ref Expression
Assertion br2base 
|- U. ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) = ( RR X. RR )

Proof

Step Hyp Ref Expression
1 brsigasspwrn 
 |-  BrSiga C_ ~P RR
2 1 sseli 
 |-  ( x e. BrSiga -> x e. ~P RR )
3 2 elpwid 
 |-  ( x e. BrSiga -> x C_ RR )
4 1 sseli 
 |-  ( y e. BrSiga -> y e. ~P RR )
5 4 elpwid 
 |-  ( y e. BrSiga -> y C_ RR )
6 xpss12 
 |-  ( ( x C_ RR /\ y C_ RR ) -> ( x X. y ) C_ ( RR X. RR ) )
7 3 5 6 syl2an 
 |-  ( ( x e. BrSiga /\ y e. BrSiga ) -> ( x X. y ) C_ ( RR X. RR ) )
8 vex 
 |-  x e. _V
9 vex 
 |-  y e. _V
10 8 9 xpex 
 |-  ( x X. y ) e. _V
11 10 elpw 
 |-  ( ( x X. y ) e. ~P ( RR X. RR ) <-> ( x X. y ) C_ ( RR X. RR ) )
12 7 11 sylibr 
 |-  ( ( x e. BrSiga /\ y e. BrSiga ) -> ( x X. y ) e. ~P ( RR X. RR ) )
13 12 rgen2 
 |-  A. x e. BrSiga A. y e. BrSiga ( x X. y ) e. ~P ( RR X. RR )
14 eqid 
 |-  ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) = ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) )
15 14 rnmposs 
 |-  ( A. x e. BrSiga A. y e. BrSiga ( x X. y ) e. ~P ( RR X. RR ) -> ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) C_ ~P ( RR X. RR ) )
16 13 15 ax-mp 
 |-  ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) C_ ~P ( RR X. RR )
17 unibrsiga 
 |-  U. BrSiga = RR
18 brsigarn 
 |-  BrSiga e. ( sigAlgebra ` RR )
19 elrnsiga 
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga e. U. ran sigAlgebra )
20 unielsiga 
 |-  ( BrSiga e. U. ran sigAlgebra -> U. BrSiga e. BrSiga )
21 18 19 20 mp2b 
 |-  U. BrSiga e. BrSiga
22 17 21 eqeltrri 
 |-  RR e. BrSiga
23 eqid 
 |-  ( RR X. RR ) = ( RR X. RR )
24 xpeq1 
 |-  ( x = RR -> ( x X. y ) = ( RR X. y ) )
25 24 eqeq2d 
 |-  ( x = RR -> ( ( RR X. RR ) = ( x X. y ) <-> ( RR X. RR ) = ( RR X. y ) ) )
26 xpeq2 
 |-  ( y = RR -> ( RR X. y ) = ( RR X. RR ) )
27 26 eqeq2d 
 |-  ( y = RR -> ( ( RR X. RR ) = ( RR X. y ) <-> ( RR X. RR ) = ( RR X. RR ) ) )
28 25 27 rspc2ev 
 |-  ( ( RR e. BrSiga /\ RR e. BrSiga /\ ( RR X. RR ) = ( RR X. RR ) ) -> E. x e. BrSiga E. y e. BrSiga ( RR X. RR ) = ( x X. y ) )
29 22 22 23 28 mp3an 
 |-  E. x e. BrSiga E. y e. BrSiga ( RR X. RR ) = ( x X. y )
30 14 10 elrnmpo 
 |-  ( ( RR X. RR ) e. ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) <-> E. x e. BrSiga E. y e. BrSiga ( RR X. RR ) = ( x X. y ) )
31 29 30 mpbir 
 |-  ( RR X. RR ) e. ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) )
32 elpwuni 
 |-  ( ( RR X. RR ) e. ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) -> ( ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) C_ ~P ( RR X. RR ) <-> U. ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) = ( RR X. RR ) ) )
33 31 32 ax-mp 
 |-  ( ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) C_ ~P ( RR X. RR ) <-> U. ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) = ( RR X. RR ) )
34 16 33 mpbi 
 |-  U. ran ( x e. BrSiga , y e. BrSiga |-> ( x X. y ) ) = ( RR X. RR )