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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
Assertion sxbrsigalem4 ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) = ( sigaGen ‘ ran 𝑅 )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
4 1 2 3 sxbrsigalem1 ⊢ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ran 𝑅 )
5 1 2 3 sxbrsigalem2 ⊢ ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) )
6 1 sxbrsigalem3 ⊢ ( sigaGen ‘ ( ran ( 𝑒 ∈ ℝ ↦ ( ( 𝑒 [,) +∞ ) × ℝ ) ) ∪ ran ( 𝑓 ∈ ℝ ↦ ( ℝ × ( 𝑓 [,) +∞ ) ) ) ) ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
7 5 6 sstri ⊢ ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) )
8 1 tpr2tp ⊢ ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ℝ × ℝ ) )
9 8 topontopi ⊢ ( 𝐽 ×t 𝐽 ) ∈ Top
10 eqid ⊢ ∪ ( 𝐽 ×t 𝐽 ) = ∪ ( 𝐽 ×t 𝐽 )
11 9 10 unicls ⊢ ∪ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) = ∪ ( 𝐽 ×t 𝐽 )
12 cldssbrsiga ⊢ ( ( 𝐽 ×t 𝐽 ) ∈ Top → ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) )
13 9 12 ax-mp ⊢ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) )
14 sigagenss2 ⊢ ( ( ∪ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) = ∪ ( 𝐽 ×t 𝐽 ) ∧ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ⊆ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) ∧ ( 𝐽 ×t 𝐽 ) ∈ Top ) → ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) ⊆ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) )
15 11 13 9 14 mp3an ⊢ ( sigaGen ‘ ( Clsd ‘ ( 𝐽 ×t 𝐽 ) ) ) ⊆ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) )
16 7 15 sstri ⊢ ( sigaGen ‘ ran 𝑅 ) ⊆ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) )
17 4 16 eqssi ⊢ ( sigaGen ‘ ( 𝐽 ×t 𝐽 ) ) = ( sigaGen ‘ ran 𝑅 )