Metamath Proof Explorer

Theorem sxbrsigalem3

Description: The sigma-algebra generated by the closed half-spaces of ( RR X. RR ) is a subset of the sigma-algebra generated by the closed sets of ( RR X. RR ) . (Contributed by Thierry Arnoux, 11-Oct-2017)

Ref Expression
Hypothesis sxbrsiga.0 
|- J = ( topGen ` ran (,) )
Assertion sxbrsigalem3 
|- ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 
 |-  J = ( topGen ` ran (,) )
2 sxbrsigalem0 
 |-  U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = ( RR X. RR )
3 retop 
 |-  ( topGen ` ran (,) ) e. Top
4 1 3 eqeltri 
 |-  J e. Top
5 4 4 txtopi 
 |-  ( J tX J ) e. Top
6 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
7 1 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
8 6 7 eqtr4i 
 |-  RR = U. J
9 4 4 8 8 txunii 
 |-  ( RR X. RR ) = U. ( J tX J )
10 5 9 unicls 
 |-  U. ( Clsd ` ( J tX J ) ) = ( RR X. RR )
11 2 10 eqtr4i 
 |-  U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = U. ( Clsd ` ( J tX J ) )
12 ovex 
 |-  ( e [,) +oo ) e. _V
13 reex 
 |-  RR e. _V
14 12 13 xpex 
 |-  ( ( e [,) +oo ) X. RR ) e. _V
15 eqid 
 |-  ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) = ( e e. RR |-> ( ( e [,) +oo ) X. RR ) )
16 14 15 fnmpti 
 |-  ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) Fn RR
17 oveq1 
 |-  ( e = u -> ( e [,) +oo ) = ( u [,) +oo ) )
18 17 xpeq1d 
 |-  ( e = u -> ( ( e [,) +oo ) X. RR ) = ( ( u [,) +oo ) X. RR ) )
19 ovex 
 |-  ( u [,) +oo ) e. _V
20 19 13 xpex 
 |-  ( ( u [,) +oo ) X. RR ) e. _V
21 18 15 20 fvmpt 
 |-  ( u e. RR -> ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` u ) = ( ( u [,) +oo ) X. RR ) )
22 icopnfcld 
 |-  ( u e. RR -> ( u [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
23 1 fveq2i 
 |-  ( Clsd ` J ) = ( Clsd ` ( topGen ` ran (,) ) )
24 22 23 eleqtrrdi 
 |-  ( u e. RR -> ( u [,) +oo ) e. ( Clsd ` J ) )
25 dif0 
 |-  ( RR \ (/) ) = RR
26 0opn 
 |-  ( J e. Top -> (/) e. J )
27 4 26 ax-mp 
 |-  (/) e. J
28 8 opncld 
 |-  ( ( J e. Top /\ (/) e. J ) -> ( RR \ (/) ) e. ( Clsd ` J ) )
29 4 27 28 mp2an 
 |-  ( RR \ (/) ) e. ( Clsd ` J )
30 25 29 eqeltrri 
 |-  RR e. ( Clsd ` J )
31 txcld 
 |-  ( ( ( u [,) +oo ) e. ( Clsd ` J ) /\ RR e. ( Clsd ` J ) ) -> ( ( u [,) +oo ) X. RR ) e. ( Clsd ` ( J tX J ) ) )
32 24 30 31 sylancl 
 |-  ( u e. RR -> ( ( u [,) +oo ) X. RR ) e. ( Clsd ` ( J tX J ) ) )
33 21 32 eqeltrd 
 |-  ( u e. RR -> ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` u ) e. ( Clsd ` ( J tX J ) ) )
34 33 rgen 
 |-  A. u e. RR ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` u ) e. ( Clsd ` ( J tX J ) )
35 fnfvrnss 
 |-  ( ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) Fn RR /\ A. u e. RR ( ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) ` u ) e. ( Clsd ` ( J tX J ) ) ) -> ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) C_ ( Clsd ` ( J tX J ) ) )
36 16 34 35 mp2an 
 |-  ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) C_ ( Clsd ` ( J tX J ) )
37 ovex 
 |-  ( f [,) +oo ) e. _V
38 13 37 xpex 
 |-  ( RR X. ( f [,) +oo ) ) e. _V
39 eqid 
 |-  ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) = ( f e. RR |-> ( RR X. ( f [,) +oo ) ) )
40 38 39 fnmpti 
 |-  ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) Fn RR
41 oveq1 
 |-  ( f = v -> ( f [,) +oo ) = ( v [,) +oo ) )
42 41 xpeq2d 
 |-  ( f = v -> ( RR X. ( f [,) +oo ) ) = ( RR X. ( v [,) +oo ) ) )
43 ovex 
 |-  ( v [,) +oo ) e. _V
44 13 43 xpex 
 |-  ( RR X. ( v [,) +oo ) ) e. _V
45 42 39 44 fvmpt 
 |-  ( v e. RR -> ( ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ` v ) = ( RR X. ( v [,) +oo ) ) )
46 icopnfcld 
 |-  ( v e. RR -> ( v [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
47 46 23 eleqtrrdi 
 |-  ( v e. RR -> ( v [,) +oo ) e. ( Clsd ` J ) )
48 txcld 
 |-  ( ( RR e. ( Clsd ` J ) /\ ( v [,) +oo ) e. ( Clsd ` J ) ) -> ( RR X. ( v [,) +oo ) ) e. ( Clsd ` ( J tX J ) ) )
49 30 47 48 sylancr 
 |-  ( v e. RR -> ( RR X. ( v [,) +oo ) ) e. ( Clsd ` ( J tX J ) ) )
50 45 49 eqeltrd 
 |-  ( v e. RR -> ( ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ` v ) e. ( Clsd ` ( J tX J ) ) )
51 50 rgen 
 |-  A. v e. RR ( ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ` v ) e. ( Clsd ` ( J tX J ) )
52 fnfvrnss 
 |-  ( ( ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) Fn RR /\ A. v e. RR ( ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ` v ) e. ( Clsd ` ( J tX J ) ) ) -> ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) C_ ( Clsd ` ( J tX J ) ) )
53 40 51 52 mp2an 
 |-  ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) C_ ( Clsd ` ( J tX J ) )
54 36 53 unssi 
 |-  ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) C_ ( Clsd ` ( J tX J ) )
55 fvex 
 |-  ( Clsd ` ( J tX J ) ) e. _V
56 sssigagen 
 |-  ( ( Clsd ` ( J tX J ) ) e. _V -> ( Clsd ` ( J tX J ) ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) ) )
57 55 56 ax-mp 
 |-  ( Clsd ` ( J tX J ) ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) )
58 54 57 sstri 
 |-  ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) )
59 sigagenss2 
 |-  ( ( U. ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) = U. ( Clsd ` ( J tX J ) ) /\ ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) ) /\ ( Clsd ` ( J tX J ) ) e. _V ) -> ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) ) )
60 11 58 55 59 mp3an 
 |-  ( sigaGen ` ( ran ( e e. RR |-> ( ( e [,) +oo ) X. RR ) ) u. ran ( f e. RR |-> ( RR X. ( f [,) +oo ) ) ) ) ) C_ ( sigaGen ` ( Clsd ` ( J tX J ) ) )