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

Theorem measbase 33264
Description: The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
Assertion
Ref Expression
measbase (𝑀 ∈ (measuresβ€˜π‘†) β†’ 𝑆 ∈ βˆͺ ran sigAlgebra)

Proof of Theorem measbase
Dummy variables π‘₯ π‘š 𝑦 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvdm 6928 . 2 (𝑀 ∈ (measuresβ€˜π‘†) β†’ 𝑆 ∈ dom measures)
2 vex 3478 . . . . 5 𝑠 ∈ V
3 ovex 7444 . . . . 5 (0[,]+∞) ∈ V
4 mapex 8828 . . . . 5 ((𝑠 ∈ V ∧ (0[,]+∞) ∈ V) β†’ {π‘š ∣ π‘š:π‘ βŸΆ(0[,]+∞)} ∈ V)
52, 3, 4mp2an 690 . . . 4 {π‘š ∣ π‘š:π‘ βŸΆ(0[,]+∞)} ∈ V
6 simp1 1136 . . . . 5 ((π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦))) β†’ π‘š:π‘ βŸΆ(0[,]+∞))
76ss2abi 4063 . . . 4 {π‘š ∣ (π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)))} βŠ† {π‘š ∣ π‘š:π‘ βŸΆ(0[,]+∞)}
85, 7ssexi 5322 . . 3 {π‘š ∣ (π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)))} ∈ V
9 df-meas 33263 . . 3 measures = (𝑠 ∈ βˆͺ ran sigAlgebra ↦ {π‘š ∣ (π‘š:π‘ βŸΆ(0[,]+∞) ∧ (π‘šβ€˜βˆ…) = 0 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠((π‘₯ β‰Ό Ο‰ ∧ Disj 𝑦 ∈ π‘₯ 𝑦) β†’ (π‘šβ€˜βˆͺ π‘₯) = Ξ£*𝑦 ∈ π‘₯(π‘šβ€˜π‘¦)))})
108, 9dmmpti 6694 . 2 dom measures = βˆͺ ran sigAlgebra
111, 10eleqtrdi 2843 1 (𝑀 ∈ (measuresβ€˜π‘†) β†’ 𝑆 ∈ βˆͺ ran sigAlgebra)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  {cab 2709  βˆ€wral 3061  Vcvv 3474  βˆ…c0 4322  π’« cpw 4602  βˆͺ cuni 4908  Disj wdisj 5113   class class class wbr 5148  dom cdm 5676  ran crn 5677  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  Ο‰com 7857   β‰Ό cdom 8939  0cc0 11112  +∞cpnf 11247  [,]cicc 13329  Ξ£*cesum 33094  sigAlgebracsiga 33175  measurescmeas 33262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7414  df-meas 33263
This theorem is referenced by:  measfrge0  33270  measvnul  33273  measvun  33276  measxun2  33277  measun  33278  measvuni  33281  measssd  33282  measunl  33283  measiuns  33284  measiun  33285  meascnbl  33286  measinblem  33287  measinb  33288  measinb2  33290  measdivcst  33291  measdivcstALTV  33292  aean  33311  domprobsiga  33479  prob01  33481  probfinmeasb  33496  probfinmeasbALTV  33497  probmeasb  33498
  Copyright terms: Public domain W3C validator