Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  meadjuni Structured version   Visualization version   GIF version

Theorem meadjuni 41612
Description: The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
meadjuni.m (𝜑𝑀 ∈ Meas)
meadjuni.s 𝑆 = dom 𝑀
meadjuni.x (𝜑𝑋𝑆)
meadjuni.cnb (𝜑𝑋 ≼ ω)
meadjuni.dj (𝜑Disj 𝑥𝑋 𝑥)
Assertion
Ref Expression
meadjuni (𝜑 → (𝑀 𝑋) = (Σ^‘(𝑀𝑋)))
Distinct variable group:   𝑥,𝑋
Allowed substitution hints:   𝜑(𝑥)   𝑆(𝑥)   𝑀(𝑥)

Proof of Theorem meadjuni
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 meadjuni.cnb . . 3 (𝜑𝑋 ≼ ω)
2 meadjuni.dj . . 3 (𝜑Disj 𝑥𝑋 𝑥)
31, 2jca 507 . 2 (𝜑 → (𝑋 ≼ ω ∧ Disj 𝑥𝑋 𝑥))
4 meadjuni.x . . . . 5 (𝜑𝑋𝑆)
5 meadjuni.s . . . . 5 𝑆 = dom 𝑀
64, 5syl6sseq 3870 . . . 4 (𝜑𝑋 ⊆ dom 𝑀)
7 meadjuni.m . . . . . . 7 (𝜑𝑀 ∈ Meas)
87, 5dmmeasal 41607 . . . . . 6 (𝜑𝑆 ∈ SAlg)
98, 4ssexd 5044 . . . . 5 (𝜑𝑋 ∈ V)
10 elpwg 4387 . . . . 5 (𝑋 ∈ V → (𝑋 ∈ 𝒫 dom 𝑀𝑋 ⊆ dom 𝑀))
119, 10syl 17 . . . 4 (𝜑 → (𝑋 ∈ 𝒫 dom 𝑀𝑋 ⊆ dom 𝑀))
126, 11mpbird 249 . . 3 (𝜑𝑋 ∈ 𝒫 dom 𝑀)
13 ismea 41606 . . . . 5 (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑥𝑦 𝑥) → (𝑀 𝑦) = (Σ^‘(𝑀𝑦)))))
147, 13sylib 210 . . . 4 (𝜑 → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑥𝑦 𝑥) → (𝑀 𝑦) = (Σ^‘(𝑀𝑦)))))
1514simprd 491 . . 3 (𝜑 → ∀𝑦 ∈ 𝒫 dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑥𝑦 𝑥) → (𝑀 𝑦) = (Σ^‘(𝑀𝑦))))
16 breq1 4891 . . . . . 6 (𝑦 = 𝑋 → (𝑦 ≼ ω ↔ 𝑋 ≼ ω))
17 disjeq1 4863 . . . . . 6 (𝑦 = 𝑋 → (Disj 𝑥𝑦 𝑥Disj 𝑥𝑋 𝑥))
1816, 17anbi12d 624 . . . . 5 (𝑦 = 𝑋 → ((𝑦 ≼ ω ∧ Disj 𝑥𝑦 𝑥) ↔ (𝑋 ≼ ω ∧ Disj 𝑥𝑋 𝑥)))
19 unieq 4681 . . . . . . 7 (𝑦 = 𝑋 𝑦 = 𝑋)
2019fveq2d 6452 . . . . . 6 (𝑦 = 𝑋 → (𝑀 𝑦) = (𝑀 𝑋))
21 reseq2 5639 . . . . . . 7 (𝑦 = 𝑋 → (𝑀𝑦) = (𝑀𝑋))
2221fveq2d 6452 . . . . . 6 (𝑦 = 𝑋 → (Σ^‘(𝑀𝑦)) = (Σ^‘(𝑀𝑋)))
2320, 22eqeq12d 2793 . . . . 5 (𝑦 = 𝑋 → ((𝑀 𝑦) = (Σ^‘(𝑀𝑦)) ↔ (𝑀 𝑋) = (Σ^‘(𝑀𝑋))))
2418, 23imbi12d 336 . . . 4 (𝑦 = 𝑋 → (((𝑦 ≼ ω ∧ Disj 𝑥𝑦 𝑥) → (𝑀 𝑦) = (Σ^‘(𝑀𝑦))) ↔ ((𝑋 ≼ ω ∧ Disj 𝑥𝑋 𝑥) → (𝑀 𝑋) = (Σ^‘(𝑀𝑋)))))
2524rspcva 3509 . . 3 ((𝑋 ∈ 𝒫 dom 𝑀 ∧ ∀𝑦 ∈ 𝒫 dom 𝑀((𝑦 ≼ ω ∧ Disj 𝑥𝑦 𝑥) → (𝑀 𝑦) = (Σ^‘(𝑀𝑦)))) → ((𝑋 ≼ ω ∧ Disj 𝑥𝑋 𝑥) → (𝑀 𝑋) = (Σ^‘(𝑀𝑋))))
2612, 15, 25syl2anc 579 . 2 (𝜑 → ((𝑋 ≼ ω ∧ Disj 𝑥𝑋 𝑥) → (𝑀 𝑋) = (Σ^‘(𝑀𝑋))))
273, 26mpd 15 1 (𝜑 → (𝑀 𝑋) = (Σ^‘(𝑀𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  wral 3090  Vcvv 3398  wss 3792  c0 4141  𝒫 cpw 4379   cuni 4673  Disj wdisj 4856   class class class wbr 4888  dom cdm 5357  cres 5359  wf 6133  cfv 6137  (class class class)co 6924  ωcom 7345  cdom 8241  0cc0 10274  +∞cpnf 10410  [,]cicc 12495  SAlgcsalg 41466  Σ^csumge0 41517  Meascmea 41604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pr 5140
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-iun 4757  df-disj 4857  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-mea 41605
This theorem is referenced by:  meadjun  41617  meadjiun  41621
  Copyright terms: Public domain W3C validator