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