Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dya2icobrsiga Structured version   Visualization version   GIF version

Theorem dya2icobrsiga 30131
 Description: Dyadic intervals are Borel sets of ℝ. (Contributed by Thierry Arnoux, 22-Sep-2017.) (Revised by Thierry Arnoux, 13-Oct-2017.)
Hypotheses
Ref Expression
sxbrsiga.0 𝐽 = (topGen‘ran (,))
dya2ioc.1 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
Assertion
Ref Expression
dya2icobrsiga ran 𝐼 ⊆ 𝔅
Distinct variable group:   𝑥,𝑛
Allowed substitution hints:   𝐼(𝑥,𝑛)   𝐽(𝑥,𝑛)

Proof of Theorem dya2icobrsiga
Dummy variable 𝑑 is distinct from all other variables.
StepHypRef Expression
1 dya2ioc.1 . . . 4 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
2 ovex 6635 . . . 4 ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈ V
31, 2elrnmpt2 6729 . . 3 (𝑑 ∈ ran 𝐼 ↔ ∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
4 simpr 477 . . . . . 6 (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
5 mnfxr 10043 . . . . . . . . . 10 -∞ ∈ ℝ*
65a1i 11 . . . . . . . . 9 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → -∞ ∈ ℝ*)
7 simpl 473 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ∈ ℤ)
87zred 11429 . . . . . . . . . . 11 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ∈ ℝ)
9 2rp 11784 . . . . . . . . . . . . 13 2 ∈ ℝ+
109a1i 11 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 2 ∈ ℝ+)
11 simpr 477 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
1210, 11rpexpcld 12975 . . . . . . . . . . 11 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2↑𝑛) ∈ ℝ+)
138, 12rerpdivcld 11850 . . . . . . . . . 10 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ∈ ℝ)
1413rexrd 10036 . . . . . . . . 9 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ∈ ℝ*)
15 1red 10002 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 1 ∈ ℝ)
168, 15readdcld 10016 . . . . . . . . . . 11 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 + 1) ∈ ℝ)
1716, 12rerpdivcld 11850 . . . . . . . . . 10 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ)
1817rexrd 10036 . . . . . . . . 9 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ*)
19 mnflt 11904 . . . . . . . . . 10 ((𝑥 / (2↑𝑛)) ∈ ℝ → -∞ < (𝑥 / (2↑𝑛)))
2013, 19syl 17 . . . . . . . . 9 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → -∞ < (𝑥 / (2↑𝑛)))
21 difioo 29400 . . . . . . . . 9 (((-∞ ∈ ℝ* ∧ (𝑥 / (2↑𝑛)) ∈ ℝ* ∧ ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ*) ∧ -∞ < (𝑥 / (2↑𝑛))) → ((-∞(,)((𝑥 + 1) / (2↑𝑛))) ∖ (-∞(,)(𝑥 / (2↑𝑛)))) = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
226, 14, 18, 20, 21syl31anc 1326 . . . . . . . 8 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((-∞(,)((𝑥 + 1) / (2↑𝑛))) ∖ (-∞(,)(𝑥 / (2↑𝑛)))) = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
23 brsigarn 30040 . . . . . . . . . 10 𝔅 ∈ (sigAlgebra‘ℝ)
24 elrnsiga 29982 . . . . . . . . . 10 (𝔅 ∈ (sigAlgebra‘ℝ) → 𝔅 ran sigAlgebra)
2523, 24ax-mp 5 . . . . . . . . 9 𝔅 ran sigAlgebra
26 retop 22478 . . . . . . . . . . 11 (topGen‘ran (,)) ∈ Top
27 iooretop 22482 . . . . . . . . . . 11 (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ (topGen‘ran (,))
28 elsigagen 30003 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ (topGen‘ran (,))) → (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ (sigaGen‘(topGen‘ran (,))))
2926, 27, 28mp2an 707 . . . . . . . . . 10 (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ (sigaGen‘(topGen‘ran (,)))
30 df-brsiga 30038 . . . . . . . . . 10 𝔅 = (sigaGen‘(topGen‘ran (,)))
3129, 30eleqtrri 2697 . . . . . . . . 9 (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ 𝔅
32 iooretop 22482 . . . . . . . . . . 11 (-∞(,)(𝑥 / (2↑𝑛))) ∈ (topGen‘ran (,))
33 elsigagen 30003 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (-∞(,)(𝑥 / (2↑𝑛))) ∈ (topGen‘ran (,))) → (-∞(,)(𝑥 / (2↑𝑛))) ∈ (sigaGen‘(topGen‘ran (,))))
3426, 32, 33mp2an 707 . . . . . . . . . 10 (-∞(,)(𝑥 / (2↑𝑛))) ∈ (sigaGen‘(topGen‘ran (,)))
3534, 30eleqtrri 2697 . . . . . . . . 9 (-∞(,)(𝑥 / (2↑𝑛))) ∈ 𝔅
36 difelsiga 29989 . . . . . . . . 9 ((𝔅 ran sigAlgebra ∧ (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ 𝔅 ∧ (-∞(,)(𝑥 / (2↑𝑛))) ∈ 𝔅) → ((-∞(,)((𝑥 + 1) / (2↑𝑛))) ∖ (-∞(,)(𝑥 / (2↑𝑛)))) ∈ 𝔅)
3725, 31, 35, 36mp3an 1421 . . . . . . . 8 ((-∞(,)((𝑥 + 1) / (2↑𝑛))) ∖ (-∞(,)(𝑥 / (2↑𝑛)))) ∈ 𝔅
3822, 37syl6eqelr 2707 . . . . . . 7 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈ 𝔅)
3938adantr 481 . . . . . 6 (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈ 𝔅)
404, 39eqeltrd 2698 . . . . 5 (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑑 ∈ 𝔅)
4140ex 450 . . . 4 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → 𝑑 ∈ 𝔅))
4241rexlimivv 3029 . . 3 (∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → 𝑑 ∈ 𝔅)
433, 42sylbi 207 . 2 (𝑑 ∈ ran 𝐼𝑑 ∈ 𝔅)
4443ssriv 3588 1 ran 𝐼 ⊆ 𝔅
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∃wrex 2908   ∖ cdif 3553   ⊆ wss 3556  ∪ cuni 4404   class class class wbr 4615  ran crn 5077  ‘cfv 5849  (class class class)co 6607   ↦ cmpt2 6609  ℝcr 9882  1c1 9884   + caddc 9886  -∞cmnf 10019  ℝ*cxr 10020   < clt 10021   / cdiv 10631  2c2 11017  ℤcz 11324  ℝ+crp 11779  (,)cioo 12120  [,)cico 12122  ↑cexp 12803  topGenctg 16022  Topctop 20620  sigAlgebracsiga 29963  sigaGencsigagen 29994  𝔅ℝcbrsiga 30037 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-inf2 8485  ax-ac2 9232  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-se 5036  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-isom 5858  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-2o 7509  df-oadd 7512  df-er 7690  df-map 7807  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-sup 8295  df-inf 8296  df-oi 8362  df-card 8712  df-acn 8715  df-ac 8886  df-cda 8937  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-n0 11240  df-z 11325  df-uz 11635  df-q 11736  df-rp 11780  df-ioo 12124  df-ico 12126  df-seq 12745  df-exp 12804  df-topgen 16028  df-top 20621  df-bases 20664  df-siga 29964  df-sigagen 29995  df-brsiga 30038 This theorem is referenced by:  sxbrsigalem2  30141  sxbrsigalem5  30143
 Copyright terms: Public domain W3C validator