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

Theorem sxbrsigalem1 31179
Description: The Borel algebra on (ℝ × ℝ) is a subset of the sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of (ℝ × ℝ). This is a step of the proof of Proposition 1.1.5 of [Cohn] p. 4. (Contributed by Thierry Arnoux, 17-Sep-2017.)
Hypotheses
Ref Expression
sxbrsiga.0 𝐽 = (topGen‘ran (,))
dya2ioc.1 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
dya2ioc.2 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))
Assertion
Ref Expression
sxbrsigalem1 (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (sigaGen‘ran 𝑅)
Distinct variable groups:   𝑥,𝑛   𝑥,𝐼   𝑣,𝑢,𝐼,𝑥   𝑢,𝑛,𝑣   𝑅,𝑛,𝑥   𝑥,𝐽
Allowed substitution hints:   𝑅(𝑣,𝑢)   𝐼(𝑛)   𝐽(𝑣,𝑢,𝑛)

Proof of Theorem sxbrsigalem1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 sxbrsiga.0 . . . 4 𝐽 = (topGen‘ran (,))
2 dya2ioc.1 . . . 4 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))
3 dya2ioc.2 . . . 4 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))
41, 2, 3dya2iocucvr 31178 . . 3 ran 𝑅 = (ℝ × ℝ)
5 retop 23067 . . . . 5 (topGen‘ran (,)) ∈ Top
61, 5eqeltri 2859 . . . 4 𝐽 ∈ Top
7 uniretop 23068 . . . . 5 ℝ = (topGen‘ran (,))
81unieqi 4719 . . . . 5 𝐽 = (topGen‘ran (,))
97, 8eqtr4i 2802 . . . 4 ℝ = 𝐽
106, 6, 9, 9txunii 21899 . . 3 (ℝ × ℝ) = (𝐽 ×t 𝐽)
114, 10eqtr2i 2800 . 2 (𝐽 ×t 𝐽) = ran 𝑅
121, 2, 3dya2iocuni 31177 . . . 4 (𝑥 ∈ (𝐽 ×t 𝐽) → ∃𝑦 ∈ 𝒫 ran 𝑅 𝑦 = 𝑥)
13 simpr 477 . . . . . 6 ((𝑦 ∈ 𝒫 ran 𝑅 𝑦 = 𝑥) → 𝑦 = 𝑥)
141, 2, 3dya2iocct 31174 . . . . . . . . 9 ran 𝑅 ≼ ω
15 ctex 8317 . . . . . . . . 9 (ran 𝑅 ≼ ω → ran 𝑅 ∈ V)
1614, 15mp1i 13 . . . . . . . 8 (𝑦 ∈ 𝒫 ran 𝑅 → ran 𝑅 ∈ V)
17 elpwi 4430 . . . . . . . 8 (𝑦 ∈ 𝒫 ran 𝑅𝑦 ⊆ ran 𝑅)
18 ssct 8390 . . . . . . . . 9 ((𝑦 ⊆ ran 𝑅 ∧ ran 𝑅 ≼ ω) → 𝑦 ≼ ω)
1917, 14, 18sylancl 577 . . . . . . . 8 (𝑦 ∈ 𝒫 ran 𝑅𝑦 ≼ ω)
20 elsigagen2 31043 . . . . . . . 8 ((ran 𝑅 ∈ V ∧ 𝑦 ⊆ ran 𝑅𝑦 ≼ ω) → 𝑦 ∈ (sigaGen‘ran 𝑅))
2116, 17, 19, 20syl3anc 1351 . . . . . . 7 (𝑦 ∈ 𝒫 ran 𝑅 𝑦 ∈ (sigaGen‘ran 𝑅))
2221adantr 473 . . . . . 6 ((𝑦 ∈ 𝒫 ran 𝑅 𝑦 = 𝑥) → 𝑦 ∈ (sigaGen‘ran 𝑅))
2313, 22eqeltrrd 2864 . . . . 5 ((𝑦 ∈ 𝒫 ran 𝑅 𝑦 = 𝑥) → 𝑥 ∈ (sigaGen‘ran 𝑅))
2423rexlimiva 3223 . . . 4 (∃𝑦 ∈ 𝒫 ran 𝑅 𝑦 = 𝑥𝑥 ∈ (sigaGen‘ran 𝑅))
2512, 24syl 17 . . 3 (𝑥 ∈ (𝐽 ×t 𝐽) → 𝑥 ∈ (sigaGen‘ran 𝑅))
2625ssriv 3861 . 2 (𝐽 ×t 𝐽) ⊆ (sigaGen‘ran 𝑅)
2714, 15ax-mp 5 . 2 ran 𝑅 ∈ V
28 sigagenss2 31045 . 2 (( (𝐽 ×t 𝐽) = ran 𝑅 ∧ (𝐽 ×t 𝐽) ⊆ (sigaGen‘ran 𝑅) ∧ ran 𝑅 ∈ V) → (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (sigaGen‘ran 𝑅))
2911, 26, 27, 28mp3an 1440 1 (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (sigaGen‘ran 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wa 387   = wceq 1507  wcel 2048  wrex 3086  Vcvv 3412  wss 3828  𝒫 cpw 4420   cuni 4710   class class class wbr 4927   × cxp 5402  ran crn 5405  cfv 6186  (class class class)co 6974  cmpo 6976  ωcom 7394  cdom 8300  cr 10330  1c1 10332   + caddc 10334   / cdiv 11094  2c2 11492  cz 11790  (,)cioo 12551  [,)cico 12553  cexp 13241  topGenctg 16561  Topctop 21199   ×t ctx 21866  sigaGencsigagen 31033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-rep 5047  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-inf2 8894  ax-ac2 9679  ax-cnex 10387  ax-resscn 10388  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-addrcl 10392  ax-mulcl 10393  ax-mulrcl 10394  ax-mulcom 10395  ax-addass 10396  ax-mulass 10397  ax-distr 10398  ax-i2m1 10399  ax-1ne0 10400  ax-1rid 10401  ax-rnegex 10402  ax-rrecex 10403  ax-cnre 10404  ax-pre-lttri 10405  ax-pre-lttrn 10406  ax-pre-ltadd 10407  ax-pre-mulgt0 10408  ax-pre-sup 10409  ax-addf 10410  ax-mulf 10411
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-nel 3071  df-ral 3090  df-rex 3091  df-reu 3092  df-rmo 3093  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-int 4748  df-iun 4792  df-iin 4793  df-br 4928  df-opab 4990  df-mpt 5007  df-tr 5029  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-isom 6195  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-of 7225  df-om 7395  df-1st 7498  df-2nd 7499  df-supp 7631  df-wrecs 7747  df-recs 7809  df-rdg 7847  df-1o 7901  df-2o 7902  df-oadd 7905  df-omul 7906  df-er 8085  df-map 8204  df-pm 8205  df-ixp 8256  df-en 8303  df-dom 8304  df-sdom 8305  df-fin 8306  df-fsupp 8625  df-fi 8666  df-sup 8697  df-inf 8698  df-oi 8765  df-card 9158  df-acn 9161  df-ac 9332  df-cda 9384  df-pnf 10472  df-mnf 10473  df-xr 10474  df-ltxr 10475  df-le 10476  df-sub 10668  df-neg 10669  df-div 11095  df-nn 11436  df-2 11500  df-3 11501  df-4 11502  df-5 11503  df-6 11504  df-7 11505  df-8 11506  df-9 11507  df-n0 11705  df-z 11791  df-dec 11909  df-uz 12056  df-q 12160  df-rp 12202  df-xneg 12321  df-xadd 12322  df-xmul 12323  df-ioo 12555  df-ioc 12556  df-ico 12557  df-icc 12558  df-fz 12706  df-fzo 12847  df-fl 12974  df-mod 13050  df-seq 13182  df-exp 13242  df-fac 13446  df-bc 13475  df-hash 13503  df-shft 14281  df-cj 14313  df-re 14314  df-im 14315  df-sqrt 14449  df-abs 14450  df-limsup 14683  df-clim 14700  df-rlim 14701  df-sum 14898  df-ef 15275  df-sin 15277  df-cos 15278  df-pi 15280  df-struct 16335  df-ndx 16336  df-slot 16337  df-base 16339  df-sets 16340  df-ress 16341  df-plusg 16428  df-mulr 16429  df-starv 16430  df-sca 16431  df-vsca 16432  df-ip 16433  df-tset 16434  df-ple 16435  df-ds 16437  df-unif 16438  df-hom 16439  df-cco 16440  df-rest 16546  df-topn 16547  df-0g 16565  df-gsum 16566  df-topgen 16567  df-pt 16568  df-prds 16571  df-xrs 16625  df-qtop 16630  df-imas 16631  df-xps 16633  df-mre 16709  df-mrc 16710  df-acs 16712  df-mgm 17704  df-sgrp 17746  df-mnd 17757  df-submnd 17798  df-mulg 18006  df-cntz 18212  df-cmn 18662  df-psmet 20233  df-xmet 20234  df-met 20235  df-bl 20236  df-mopn 20237  df-fbas 20238  df-fg 20239  df-cnfld 20242  df-refld 20445  df-top 21200  df-topon 21217  df-topsp 21239  df-bases 21252  df-cld 21325  df-ntr 21326  df-cls 21327  df-nei 21404  df-lp 21442  df-perf 21443  df-cn 21533  df-cnp 21534  df-haus 21621  df-cmp 21693  df-tx 21868  df-hmeo 22061  df-fil 22152  df-fm 22244  df-flim 22245  df-flf 22246  df-fcls 22247  df-xms 22627  df-ms 22628  df-tms 22629  df-cncf 23183  df-cfil 23555  df-cmet 23557  df-cms 23635  df-limc 24161  df-dv 24162  df-log 24835  df-cxp 24836  df-logb 25038  df-siga 31003  df-sigagen 31034
This theorem is referenced by:  sxbrsigalem4  31181
  Copyright terms: Public domain W3C validator