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 𝐽 = ( topGen ‘ ran (,) )
Assertion sxbrsigalem3 ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 𝐽 = ( topGen ‘ ran (,) )
2 sxbrsigalem0 ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( ℝ × ℝ )
3 retop ( topGen ‘ ran (,) ) ∈ Top
4 1 3 eqeltri 𝐽 ∈ Top
5 4 4 txtopi ( 𝐽 ×t 𝐽 ) ∈ Top
6 uniretop ℝ = ( topGen ‘ ran (,) )
7 1 unieqi 𝐽 = ( topGen ‘ ran (,) )
8 6 7 eqtr4i ℝ = 𝐽
9 4 4 8 8 txunii ( ℝ × ℝ ) = ( 𝐽 ×t 𝐽 )
10 5 9 unicls ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) = ( ℝ × ℝ )
11 2 10 eqtr4i ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
12 ovex ( 𝑒 [,) +∞ ) ∈ V
13 reex ℝ ∈ V
14 12 13 xpex ( ( 𝑒 [,) +∞ ) × ℝ ) ∈ V
15 eqid ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) = ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) )
16 14 15 fnmpti ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) Fn ℝ
17 oveq1 ( 𝑒 = 𝑢 → ( 𝑒 [,) +∞ ) = ( 𝑢 [,) +∞ ) )
18 17 xpeq1d ( 𝑒 = 𝑢 → ( ( 𝑒 [,) +∞ ) × ℝ ) = ( ( 𝑢 [,) +∞ ) × ℝ ) )
19 ovex ( 𝑢 [,) +∞ ) ∈ V
20 19 13 xpex ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ V
21 18 15 20 fvmpt ( 𝑢 ∈ ℝ → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) = ( ( 𝑢 [,) +∞ ) × ℝ ) )
22 icopnfcld ( 𝑢 ∈ ℝ → ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
23 1 fveq2i ( Clsd ‘ 𝐽 ) = ( Clsd ‘ ( topGen ‘ ran (,) ) )
24 22 23 eleqtrrdi ( 𝑢 ∈ ℝ → ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) )
25 dif0 ( ℝ ∖ ∅ ) = ℝ
26 0opn ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
27 4 26 ax-mp ∅ ∈ 𝐽
28 8 opncld ( ( 𝐽 ∈ Top ∧ ∅ ∈ 𝐽 ) → ( ℝ ∖ ∅ ) ∈ ( Clsd ‘ 𝐽 ) )
29 4 27 28 mp2an ( ℝ ∖ ∅ ) ∈ ( Clsd ‘ 𝐽 )
30 25 29 eqeltrri ℝ ∈ ( Clsd ‘ 𝐽 )
31 txcld ( ( ( 𝑢 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) ∧ ℝ ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
32 24 30 31 sylancl ( 𝑢 ∈ ℝ → ( ( 𝑢 [,) +∞ ) × ℝ ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
33 21 32 eqeltrd ( 𝑢 ∈ ℝ → ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
34 33 rgen 𝑢 ∈ ℝ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
35 fnfvrnss ( ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) Fn ℝ ∧ ∀ 𝑢 ∈ ℝ ( ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ‘ 𝑢 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) → ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
36 16 34 35 mp2an ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
37 ovex ( 𝑓 [,) +∞ ) ∈ V
38 13 37 xpex ( ℝ × ( 𝑓 [,) +∞ ) ) ∈ V
39 eqid ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) = ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) )
40 38 39 fnmpti ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) Fn ℝ
41 oveq1 ( 𝑓 = 𝑣 → ( 𝑓 [,) +∞ ) = ( 𝑣 [,) +∞ ) )
42 41 xpeq2d ( 𝑓 = 𝑣 → ( ℝ × ( 𝑓 [,) +∞ ) ) = ( ℝ × ( 𝑣 [,) +∞ ) ) )
43 ovex ( 𝑣 [,) +∞ ) ∈ V
44 13 43 xpex ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ V
45 42 39 44 fvmpt ( 𝑣 ∈ ℝ → ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) = ( ℝ × ( 𝑣 [,) +∞ ) ) )
46 icopnfcld ( 𝑣 ∈ ℝ → ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
47 46 23 eleqtrrdi ( 𝑣 ∈ ℝ → ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) )
48 txcld ( ( ℝ ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑣 [,) +∞ ) ∈ ( Clsd ‘ 𝐽 ) ) → ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
49 30 47 48 sylancr ( 𝑣 ∈ ℝ → ( ℝ × ( 𝑣 [,) +∞ ) ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
50 45 49 eqeltrd ( 𝑣 ∈ ℝ → ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
51 50 rgen 𝑣 ∈ ℝ ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
52 fnfvrnss ( ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) Fn ℝ ∧ ∀ 𝑣 ∈ ℝ ( ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ‘ 𝑣 ) ∈ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) → ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
53 40 51 52 mp2an ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
54 36 53 unssi ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) )
55 fvex ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V
56 sssigagen ( ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V → ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
57 55 56 ax-mp ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
58 54 57 sstri ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
59 sigagenss2 ( ( ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) = ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∧ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) ∧ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ∈ V ) → ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) )
60 11 58 55 59 mp3an ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )