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 ⊢ 𝛔 ⁡ ran ⁡ e ∈ ℝ ⟼ e +∞ × ℝ ∪ ran ⁡ f ∈ ℝ ⟼ ℝ × f +∞ ⊆ 𝛔 ⁡ Clsd ⁡ J × t J

Proof

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