MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  voliun Structured version   Visualization version   GIF version

Theorem voliun 24307
Description: The Lebesgue measure function is countably additive. (Contributed by Mario Carneiro, 18-Mar-2014.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
Hypotheses
Ref Expression
voliun.1 𝑆 = seq1( + , 𝐺)
voliun.2 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘𝐴))
Assertion
Ref Expression
voliun ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘ 𝑛 ∈ ℕ 𝐴) = sup(ran 𝑆, ℝ*, < ))

Proof of Theorem voliun
Dummy variables 𝑖 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 486 . . . . . 6 ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → 𝐴 ∈ dom vol)
21ralimi 3075 . . . . 5 (∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → ∀𝑛 ∈ ℕ 𝐴 ∈ dom vol)
32adantr 484 . . . 4 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ 𝐴 ∈ dom vol)
4 eqid 2738 . . . . 5 (𝑛 ∈ ℕ ↦ 𝐴) = (𝑛 ∈ ℕ ↦ 𝐴)
54fmpt 6885 . . . 4 (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ↔ (𝑛 ∈ ℕ ↦ 𝐴):ℕ⟶dom vol)
63, 5sylib 221 . . 3 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (𝑛 ∈ ℕ ↦ 𝐴):ℕ⟶dom vol)
74fvmpt2 6787 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) → ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = 𝐴)
87adantrr 717 . . . . . . 7 ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ)) → ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = 𝐴)
98ralimiaa 3074 . . . . . 6 (∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → ∀𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = 𝐴)
10 disjeq2 5000 . . . . . 6 (∀𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = 𝐴 → (Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑛 ∈ ℕ 𝐴))
119, 10syl 17 . . . . 5 (∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑛 ∈ ℕ 𝐴))
1211biimpar 481 . . . 4 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))
13 nfcv 2899 . . . . 5 𝑖((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)
14 nffvmpt1 6686 . . . . 5 𝑛((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)
15 fveq2 6675 . . . . 5 (𝑛 = 𝑖 → ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖))
1613, 14, 15cbvdisj 5006 . . . 4 (Disj 𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛) ↔ Disj 𝑖 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖))
1712, 16sylib 221 . . 3 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → Disj 𝑖 ∈ ℕ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖))
18 eqid 2738 . . 3 (𝑚 ∈ ℕ ↦ (vol*‘(𝑥 ∩ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚)))) = (𝑚 ∈ ℕ ↦ (vol*‘(𝑥 ∩ ((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚))))
19 eqid 2738 . . 3 seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))))
20 nfcv 2899 . . . 4 𝑚(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))
21 nfcv 2899 . . . . 5 𝑛vol
22 nffvmpt1 6686 . . . . 5 𝑛((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚)
2321, 22nffv 6685 . . . 4 𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚))
24 2fveq3 6680 . . . 4 (𝑛 = 𝑚 → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚)))
2520, 23, 24cbvmpt 5132 . . 3 (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))) = (𝑚 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑚)))
267fveq2d 6679 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴))
2726eleq1d 2817 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) → ((vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ (vol‘𝐴) ∈ ℝ))
2827biimprd 251 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝐴 ∈ dom vol) → ((vol‘𝐴) ∈ ℝ → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ))
2928impr 458 . . . . . 6 ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ)) → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ)
3029ralimiaa 3074 . . . . 5 (∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ)
3130adantr 484 . . . 4 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ)
32 nfv 1920 . . . . 5 𝑖(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ
3321, 14nffv 6685 . . . . . 6 𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖))
3433nfel1 2915 . . . . 5 𝑛(vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ
35 2fveq3 6680 . . . . . 6 (𝑛 = 𝑖 → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)))
3635eleq1d 2817 . . . . 5 (𝑛 = 𝑖 → ((vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ))
3732, 34, 36cbvralw 3340 . . . 4 (∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) ∈ ℝ ↔ ∀𝑖 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ)
3831, 37sylib 221 . . 3 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑖 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑖)) ∈ ℝ)
396, 17, 18, 19, 25, 38voliunlem3 24305 . 2 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘ ran (𝑛 ∈ ℕ ↦ 𝐴)) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))), ℝ*, < ))
40 dfiun2g 4918 . . . . 5 (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → 𝑛 ∈ ℕ 𝐴 = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴})
413, 40syl 17 . . . 4 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → 𝑛 ∈ ℕ 𝐴 = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴})
424rnmpt 5799 . . . . 5 ran (𝑛 ∈ ℕ ↦ 𝐴) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴}
4342unieqi 4810 . . . 4 ran (𝑛 ∈ ℕ ↦ 𝐴) = {𝑥 ∣ ∃𝑛 ∈ ℕ 𝑥 = 𝐴}
4441, 43eqtr4di 2791 . . 3 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → 𝑛 ∈ ℕ 𝐴 = ran (𝑛 ∈ ℕ ↦ 𝐴))
4544fveq2d 6679 . 2 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘ 𝑛 ∈ ℕ 𝐴) = (vol‘ ran (𝑛 ∈ ℕ ↦ 𝐴)))
46 voliun.1 . . . . 5 𝑆 = seq1( + , 𝐺)
47 voliun.2 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘𝐴))
48 eqid 2738 . . . . . . . 8 ℕ = ℕ
4926adantrr 717 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ)) → (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴))
5049ralimiaa 3074 . . . . . . . . 9 (∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴))
5150adantr 484 . . . . . . . 8 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴))
52 mpteq12 5118 . . . . . . . 8 ((ℕ = ℕ ∧ ∀𝑛 ∈ ℕ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)) = (vol‘𝐴)) → (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘𝐴)))
5348, 51, 52sylancr 590 . . . . . . 7 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))) = (𝑛 ∈ ℕ ↦ (vol‘𝐴)))
5447, 53eqtr4id 2792 . . . . . 6 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛))))
5554seqeq3d 13469 . . . . 5 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))))
5646, 55syl5eq 2785 . . . 4 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → 𝑆 = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))))
5756rneqd 5782 . . 3 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → ran 𝑆 = ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))))
5857supeq1d 8984 . 2 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → sup(ran 𝑆, ℝ*, < ) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘((𝑛 ∈ ℕ ↦ 𝐴)‘𝑛)))), ℝ*, < ))
5939, 45, 583eqtr4d 2783 1 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘ 𝑛 ∈ ℕ 𝐴) = sup(ran 𝑆, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wcel 2113  {cab 2716  wral 3053  wrex 3054  cin 3843   cuni 4797   ciun 4882  Disj wdisj 4996  cmpt 5111  dom cdm 5526  ran crn 5527  wf 6336  cfv 6340  supcsup 8978  cr 10615  1c1 10617   + caddc 10619  *cxr 10753   < clt 10754  cn 11717  seqcseq 13461  vol*covol 24215  volcvol 24216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480  ax-inf2 9178  ax-cc 9936  ax-cnex 10672  ax-resscn 10673  ax-1cn 10674  ax-icn 10675  ax-addcl 10676  ax-addrcl 10677  ax-mulcl 10678  ax-mulrcl 10679  ax-mulcom 10680  ax-addass 10681  ax-mulass 10682  ax-distr 10683  ax-i2m1 10684  ax-1ne0 10685  ax-1rid 10686  ax-rnegex 10687  ax-rrecex 10688  ax-cnre 10689  ax-pre-lttri 10690  ax-pre-lttrn 10691  ax-pre-ltadd 10692  ax-pre-mulgt0 10693  ax-pre-sup 10694
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-se 5485  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7128  df-ov 7174  df-oprab 7175  df-mpo 7176  df-of 7426  df-om 7601  df-1st 7715  df-2nd 7716  df-wrecs 7977  df-recs 8038  df-rdg 8076  df-1o 8132  df-2o 8133  df-er 8321  df-map 8440  df-pm 8441  df-en 8557  df-dom 8558  df-sdom 8559  df-fin 8560  df-sup 8980  df-inf 8981  df-oi 9048  df-dju 9404  df-card 9442  df-pnf 10756  df-mnf 10757  df-xr 10758  df-ltxr 10759  df-le 10760  df-sub 10951  df-neg 10952  df-div 11377  df-nn 11718  df-2 11780  df-3 11781  df-n0 11978  df-z 12064  df-uz 12326  df-q 12432  df-rp 12474  df-xadd 12592  df-ioo 12826  df-ico 12828  df-icc 12829  df-fz 12983  df-fzo 13126  df-fl 13254  df-seq 13462  df-exp 13523  df-hash 13784  df-cj 14549  df-re 14550  df-im 14551  df-sqrt 14685  df-abs 14686  df-clim 14936  df-rlim 14937  df-sum 15137  df-xmet 20211  df-met 20212  df-ovol 24217  df-vol 24218
This theorem is referenced by:  volsup  24309  vitalilem4  24364  voliune  31767  voliunsge0lem  43544
  Copyright terms: Public domain W3C validator