Metamath Proof Explorer


Theorem dya2icobrsiga

Description: Dyadic intervals are Borel sets of RR . (Contributed by Thierry Arnoux, 22-Sep-2017) (Revised by Thierry Arnoux, 13-Oct-2017)

Ref Expression
Hypotheses sxbrsiga.0 J = topGen ran .
dya2ioc.1 I = x , n x 2 n x + 1 2 n
Assertion dya2icobrsiga ran I 𝔅

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 ovex x 2 n x + 1 2 n V
4 2 3 elrnmpo d ran I x n d = x 2 n x + 1 2 n
5 simpr x n d = x 2 n x + 1 2 n d = x 2 n x + 1 2 n
6 mnfxr −∞ *
7 6 a1i x n −∞ *
8 simpl x n x
9 8 zred x n x
10 2rp 2 +
11 10 a1i x n 2 +
12 simpr x n n
13 11 12 rpexpcld x n 2 n +
14 9 13 rerpdivcld x n x 2 n
15 14 rexrd x n x 2 n *
16 1red x n 1
17 9 16 readdcld x n x + 1
18 17 13 rerpdivcld x n x + 1 2 n
19 18 rexrd x n x + 1 2 n *
20 mnflt x 2 n −∞ < x 2 n
21 14 20 syl x n −∞ < x 2 n
22 difioo −∞ * x 2 n * x + 1 2 n * −∞ < x 2 n −∞ x + 1 2 n −∞ x 2 n = x 2 n x + 1 2 n
23 7 15 19 21 22 syl31anc x n −∞ x + 1 2 n −∞ x 2 n = x 2 n x + 1 2 n
24 brsigarn 𝔅 sigAlgebra
25 elrnsiga 𝔅 sigAlgebra 𝔅 ran sigAlgebra
26 24 25 ax-mp 𝔅 ran sigAlgebra
27 retop topGen ran . Top
28 iooretop −∞ x + 1 2 n topGen ran .
29 elsigagen topGen ran . Top −∞ x + 1 2 n topGen ran . −∞ x + 1 2 n 𝛔 topGen ran .
30 27 28 29 mp2an −∞ x + 1 2 n 𝛔 topGen ran .
31 df-brsiga 𝔅 = 𝛔 topGen ran .
32 30 31 eleqtrri −∞ x + 1 2 n 𝔅
33 iooretop −∞ x 2 n topGen ran .
34 elsigagen topGen ran . Top −∞ x 2 n topGen ran . −∞ x 2 n 𝛔 topGen ran .
35 27 33 34 mp2an −∞ x 2 n 𝛔 topGen ran .
36 35 31 eleqtrri −∞ x 2 n 𝔅
37 difelsiga 𝔅 ran sigAlgebra −∞ x + 1 2 n 𝔅 −∞ x 2 n 𝔅 −∞ x + 1 2 n −∞ x 2 n 𝔅
38 26 32 36 37 mp3an −∞ x + 1 2 n −∞ x 2 n 𝔅
39 23 38 eqeltrrdi x n x 2 n x + 1 2 n 𝔅
40 39 adantr x n d = x 2 n x + 1 2 n x 2 n x + 1 2 n 𝔅
41 5 40 eqeltrd x n d = x 2 n x + 1 2 n d 𝔅
42 41 ex x n d = x 2 n x + 1 2 n d 𝔅
43 42 rexlimivv x n d = x 2 n x + 1 2 n d 𝔅
44 4 43 sylbi d ran I d 𝔅
45 44 ssriv ran I 𝔅