Metamath Proof Explorer

Theorem sxbrsigalem4

Description: The Borel algebra on ( RR X. RR ) is generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) . Proposition 1.1.5 of Cohn p. 4 . Note that the interval used in this formalization are closed-below, open-above instead of open-below, closed-above in the proof as they are ultimately generated by the floor function. (Contributed by Thierry Arnoux, 21-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
dya2ioc.1 ⊢ I = x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
dya2ioc.2 ⊢ R = u ∈ ran ⁡ I , v ∈ ran ⁡ I ⟼ u × v
Assertion sxbrsigalem4 ⊢ 𝛔 ⁡ J × t J = 𝛔 ⁡ ran ⁡ R

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ J = topGen ⁡ ran ⁡ .
2 dya2ioc.1 ⊢ I = x ∈ ℤ , n ∈ ℤ ⟼ x 2 n x + 1 2 n
3 dya2ioc.2 ⊢ R = u ∈ ran ⁡ I , v ∈ ran ⁡ I ⟼ u × v
4 1 2 3 sxbrsigalem1 ⊢ 𝛔 ⁡ J × t J ⊆ 𝛔 ⁡ ran ⁡ R
5 1 2 3 sxbrsigalem2 ⊢ 𝛔 ⁡ ran ⁡ R ⊆ 𝛔 ⁡ ran ⁡ e ∈ ℝ ⟼ e +∞ × ℝ ∪ ran ⁡ f ∈ ℝ ⟼ ℝ × f +∞
6 1 sxbrsigalem3 ⊢ 𝛔 ⁡ ran ⁡ e ∈ ℝ ⟼ e +∞ × ℝ ∪ ran ⁡ f ∈ ℝ ⟼ ℝ × f +∞ ⊆ 𝛔 ⁡ Clsd ⁡ J × t J
7 5 6 sstri ⊢ 𝛔 ⁡ ran ⁡ R ⊆ 𝛔 ⁡ Clsd ⁡ J × t J
8 1 tpr2tp ⊢ J × t J ∈ TopOn ⁡ ℝ 2
9 8 topontopi ⊢ J × t J ∈ Top
10 eqid ⊢ ⋃ J × t J = ⋃ J × t J
11 9 10 unicls ⊢ ⋃ Clsd ⁡ J × t J = ⋃ J × t J
12 cldssbrsiga ⊢ J × t J ∈ Top → Clsd ⁡ J × t J ⊆ 𝛔 ⁡ J × t J
13 9 12 ax-mp ⊢ Clsd ⁡ J × t J ⊆ 𝛔 ⁡ J × t J
14 sigagenss2 ⊢ ⋃ Clsd ⁡ J × t J = ⋃ J × t J ∧ Clsd ⁡ J × t J ⊆ 𝛔 ⁡ J × t J ∧ J × t J ∈ Top → 𝛔 ⁡ Clsd ⁡ J × t J ⊆ 𝛔 ⁡ J × t J
15 11 13 9 14 mp3an ⊢ 𝛔 ⁡ Clsd ⁡ J × t J ⊆ 𝛔 ⁡ J × t J
16 7 15 sstri ⊢ 𝛔 ⁡ ran ⁡ R ⊆ 𝛔 ⁡ J × t J
17 4 16 eqssi ⊢ 𝛔 ⁡ J × t J = 𝛔 ⁡ ran ⁡ R