Metamath Proof Explorer


Theorem meascnbl

Description: A measure is continuous from below. Cf. volsup . (Contributed by Thierry Arnoux, 18-Jan-2017) (Revised by Thierry Arnoux, 11-Jul-2017)

Ref Expression
Hypotheses meascnbl.0 J=TopOpen𝑠*𝑠0+∞
meascnbl.1 φMmeasuresS
meascnbl.2 φF:S
meascnbl.3 φnFnFn+1
Assertion meascnbl φMFtJMranF

Proof

Step Hyp Ref Expression
1 meascnbl.0 J=TopOpen𝑠*𝑠0+∞
2 meascnbl.1 φMmeasuresS
3 meascnbl.2 φF:S
4 meascnbl.3 φnFnFn+1
5 2 adantr φnMmeasuresS
6 measbase MmeasuresSSransigAlgebra
7 2 6 syl φSransigAlgebra
8 7 adantr φnSransigAlgebra
9 3 ffvelrnda φnFnS
10 simpll φnk1..^nφ
11 fzossnn 1..^n
12 simpr φnk1..^nk1..^n
13 11 12 sselid φnk1..^nk
14 3 ffvelrnda φkFkS
15 10 13 14 syl2anc φnk1..^nFkS
16 15 ralrimiva φnk1..^nFkS
17 sigaclfu2 SransigAlgebrak1..^nFkSk1..^nFkS
18 8 16 17 syl2anc φnk1..^nFkS
19 difelsiga SransigAlgebraFnSk1..^nFkSFnk1..^nFkS
20 8 9 18 19 syl3anc φnFnk1..^nFkS
21 measvxrge0 MmeasuresSFnk1..^nFkSMFnk1..^nFk0+∞
22 5 20 21 syl2anc φnMFnk1..^nFk0+∞
23 fveq2 n=oFn=Fo
24 oveq2 n=o1..^n=1..^o
25 24 iuneq1d n=ok1..^nFk=k1..^oFk
26 23 25 difeq12d n=oFnk1..^nFk=Fok1..^oFk
27 26 fveq2d n=oMFnk1..^nFk=MFok1..^oFk
28 fveq2 n=pFn=Fp
29 oveq2 n=p1..^n=1..^p
30 29 iuneq1d n=pk1..^nFk=k1..^pFk
31 28 30 difeq12d n=pFnk1..^nFk=Fpk1..^pFk
32 31 fveq2d n=pMFnk1..^nFk=MFpk1..^pFk
33 1 22 27 32 esumcvg2 φi*n=1iMFnk1..^nFktJ*nMFnk1..^nFk
34 measfrge0 MmeasuresSM:S0+∞
35 2 34 syl φM:S0+∞
36 fcompt M:S0+∞F:SMF=iMFi
37 35 3 36 syl2anc φMF=iMFi
38 nfcv _nFk
39 fveq2 n=kFn=Fk
40 simpr φii
41 40 nnzd φii
42 fzval3 i1i=1..^i+1
43 41 42 syl φi1i=1..^i+1
44 43 olcd φi1i=1i=1..^i+1
45 2 adantr φiMmeasuresS
46 simpll φin1iφ
47 fzossnn 1..^i+1
48 43 eleq2d φin1in1..^i+1
49 48 biimpa φin1in1..^i+1
50 47 49 sselid φin1in
51 46 50 9 syl2anc φin1iFnS
52 38 39 44 45 51 measiuns φiMn=1iFn=*n=1iMFnk1..^nFk
53 3 ffnd φFFn
54 53 4 iuninc φin=1iFn=Fi
55 54 fveq2d φiMn=1iFn=MFi
56 52 55 eqtr3d φi*n=1iMFnk1..^nFk=MFi
57 56 mpteq2dva φi*n=1iMFnk1..^nFk=iMFi
58 37 57 eqtr4d φMF=i*n=1iMFnk1..^nFk
59 9 ralrimiva φnFnS
60 dfiun2g nFnSnFn=x|nx=Fn
61 59 60 syl φnFn=x|nx=Fn
62 fnrnfv FFnranF=x|nx=Fn
63 53 62 syl φranF=x|nx=Fn
64 63 unieqd φranF=x|nx=Fn
65 61 64 eqtr4d φnFn=ranF
66 65 fveq2d φMnFn=MranF
67 eqidd φ=
68 67 orcd φ==1..^i+1
69 38 39 68 2 9 measiuns φMnFn=*nMFnk1..^nFk
70 66 69 eqtr3d φMranF=*nMFnk1..^nFk
71 33 58 70 3brtr4d φMFtJMranF