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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
Assertion dya2icobrsiga ran 𝐼 ⊆ 𝔅ℝ

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 ovex ⊢ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ V
4 2 3 elrnmpo ⊢ ( 𝑑 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
5 simpr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
6 mnfxr ⊢ -∞ ∈ ℝ*
7 6 a1i ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → -∞ ∈ ℝ* )
8 simpl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℤ )
9 8 zred ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
10 2rp ⊢ 2 ∈ ℝ+
11 10 a1i ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 2 ∈ ℝ+ )
12 simpr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
13 11 12 rpexpcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
14 9 13 rerpdivcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
15 14 rexrd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
16 1red ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 1 ∈ ℝ )
17 9 16 readdcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 + 1 ) ∈ ℝ )
18 17 13 rerpdivcld ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
19 18 rexrd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
20 mnflt ⊢ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ → -∞ < ( 𝑥 / ( 2 ↑ 𝑛 ) ) )
21 14 20 syl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → -∞ < ( 𝑥 / ( 2 ↑ 𝑛 ) ) )
22 difioo ⊢ ( ( ( -∞ ∈ ℝ* ∧ ( 𝑥 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ∧ ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ* ) ∧ -∞ < ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) → ( ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∖ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
23 7 15 19 21 22 syl31anc ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∖ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
24 brsigarn ⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )
25 elrnsiga ⊢ ( 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) → 𝔅ℝ ∈ ∪ ran sigAlgebra )
26 24 25 ax-mp ⊢ 𝔅ℝ ∈ ∪ ran sigAlgebra
27 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
28 iooretop ⊢ ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ ( topGen ‘ ran (,) )
29 elsigagen ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ ( topGen ‘ ran (,) ) ) → ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
30 27 28 29 mp2an ⊢ ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) )
31 df-brsiga ⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )
32 30 31 eleqtrri ⊢ ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ 𝔅ℝ
33 iooretop ⊢ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ∈ ( topGen ‘ ran (,) )
34 elsigagen ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ∈ ( topGen ‘ ran (,) ) ) → ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
35 27 33 34 mp2an ⊢ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) )
36 35 31 eleqtrri ⊢ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ∈ 𝔅ℝ
37 difelsiga ⊢ ( ( 𝔅ℝ ∈ ∪ ran sigAlgebra ∧ ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ 𝔅ℝ ∧ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ∈ 𝔅ℝ ) → ( ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∖ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ) ∈ 𝔅ℝ )
38 26 32 36 37 mp3an ⊢ ( ( -∞ (,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∖ ( -∞ (,) ( 𝑥 / ( 2 ↑ 𝑛 ) ) ) ) ∈ 𝔅ℝ
39 23 38 eqeltrrdi ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ 𝔅ℝ )
40 39 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ∈ 𝔅ℝ )
41 5 40 eqeltrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) → 𝑑 ∈ 𝔅ℝ )
42 41 ex ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → 𝑑 ∈ 𝔅ℝ ) )
43 42 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑛 ∈ ℤ 𝑑 = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) → 𝑑 ∈ 𝔅ℝ )
44 4 43 sylbi ⊢ ( 𝑑 ∈ ran 𝐼 → 𝑑 ∈ 𝔅ℝ )
45 44 ssriv ⊢ ran 𝐼 ⊆ 𝔅ℝ