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 𝐽 = ( TopOpen ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) )
meascnbl.1 ( 𝜑𝑀 ∈ ( measures ‘ 𝑆 ) )
meascnbl.2 ( 𝜑𝐹 : ℕ ⟶ 𝑆 )
meascnbl.3 ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
Assertion meascnbl ( 𝜑 → ( 𝑀𝐹 ) ( ⇝𝑡𝐽 ) ( 𝑀 ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 meascnbl.0 𝐽 = ( TopOpen ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) )
2 meascnbl.1 ( 𝜑𝑀 ∈ ( measures ‘ 𝑆 ) )
3 meascnbl.2 ( 𝜑𝐹 : ℕ ⟶ 𝑆 )
4 meascnbl.3 ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
5 2 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
6 measbase ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ran sigAlgebra )
7 2 6 syl ( 𝜑𝑆 ran sigAlgebra )
8 7 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑆 ran sigAlgebra )
9 3 ffvelrnda ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ 𝑆 )
10 simpll ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝜑 )
11 fzossnn ( 1 ..^ 𝑛 ) ⊆ ℕ
12 simpr ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑘 ∈ ( 1 ..^ 𝑛 ) )
13 11 12 sselid ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑘 ∈ ℕ )
14 3 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ 𝑆 )
15 10 13 14 syl2anc ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → ( 𝐹𝑘 ) ∈ 𝑆 )
16 15 ralrimiva ( ( 𝜑𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ∈ 𝑆 )
17 sigaclfu2 ( ( 𝑆 ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ∈ 𝑆 ) → 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ∈ 𝑆 )
18 8 16 17 syl2anc ( ( 𝜑𝑛 ∈ ℕ ) → 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ∈ 𝑆 )
19 difelsiga ( ( 𝑆 ran sigAlgebra ∧ ( 𝐹𝑛 ) ∈ 𝑆 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ∈ 𝑆 ) → ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ∈ 𝑆 )
20 8 9 18 19 syl3anc ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ∈ 𝑆 )
21 measvxrge0 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ∈ 𝑆 ) → ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) ∈ ( 0 [,] +∞ ) )
22 5 20 21 syl2anc ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) ∈ ( 0 [,] +∞ ) )
23 fveq2 ( 𝑛 = 𝑜 → ( 𝐹𝑛 ) = ( 𝐹𝑜 ) )
24 oveq2 ( 𝑛 = 𝑜 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑜 ) )
25 24 iuneq1d ( 𝑛 = 𝑜 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) = 𝑘 ∈ ( 1 ..^ 𝑜 ) ( 𝐹𝑘 ) )
26 23 25 difeq12d ( 𝑛 = 𝑜 → ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) = ( ( 𝐹𝑜 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑜 ) ( 𝐹𝑘 ) ) )
27 26 fveq2d ( 𝑛 = 𝑜 → ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) = ( 𝑀 ‘ ( ( 𝐹𝑜 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑜 ) ( 𝐹𝑘 ) ) ) )
28 fveq2 ( 𝑛 = 𝑝 → ( 𝐹𝑛 ) = ( 𝐹𝑝 ) )
29 oveq2 ( 𝑛 = 𝑝 → ( 1 ..^ 𝑛 ) = ( 1 ..^ 𝑝 ) )
30 29 iuneq1d ( 𝑛 = 𝑝 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) = 𝑘 ∈ ( 1 ..^ 𝑝 ) ( 𝐹𝑘 ) )
31 28 30 difeq12d ( 𝑛 = 𝑝 → ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) = ( ( 𝐹𝑝 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑝 ) ( 𝐹𝑘 ) ) )
32 31 fveq2d ( 𝑛 = 𝑝 → ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) = ( 𝑀 ‘ ( ( 𝐹𝑝 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑝 ) ( 𝐹𝑘 ) ) ) )
33 1 22 27 32 esumcvg2 ( 𝜑 → ( 𝑖 ∈ ℕ ↦ Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) ) ( ⇝𝑡𝐽 ) Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) )
34 measfrge0 ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
35 2 34 syl ( 𝜑𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
36 fcompt ( ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℕ ⟶ 𝑆 ) → ( 𝑀𝐹 ) = ( 𝑖 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝐹𝑖 ) ) ) )
37 35 3 36 syl2anc ( 𝜑 → ( 𝑀𝐹 ) = ( 𝑖 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝐹𝑖 ) ) ) )
38 nfcv 𝑛 ( 𝐹𝑘 )
39 fveq2 ( 𝑛 = 𝑘 → ( 𝐹𝑛 ) = ( 𝐹𝑘 ) )
40 simpr ( ( 𝜑𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
41 40 nnzd ( ( 𝜑𝑖 ∈ ℕ ) → 𝑖 ∈ ℤ )
42 fzval3 ( 𝑖 ∈ ℤ → ( 1 ... 𝑖 ) = ( 1 ..^ ( 𝑖 + 1 ) ) )
43 41 42 syl ( ( 𝜑𝑖 ∈ ℕ ) → ( 1 ... 𝑖 ) = ( 1 ..^ ( 𝑖 + 1 ) ) )
44 43 olcd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 1 ... 𝑖 ) = ℕ ∨ ( 1 ... 𝑖 ) = ( 1 ..^ ( 𝑖 + 1 ) ) ) )
45 2 adantr ( ( 𝜑𝑖 ∈ ℕ ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
46 simpll ( ( ( 𝜑𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑖 ) ) → 𝜑 )
47 fzossnn ( 1 ..^ ( 𝑖 + 1 ) ) ⊆ ℕ
48 43 eleq2d ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑛 ∈ ( 1 ... 𝑖 ) ↔ 𝑛 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) ) )
49 48 biimpa ( ( ( 𝜑𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑖 ) ) → 𝑛 ∈ ( 1 ..^ ( 𝑖 + 1 ) ) )
50 47 49 sselid ( ( ( 𝜑𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑖 ) ) → 𝑛 ∈ ℕ )
51 46 50 9 syl2anc ( ( ( 𝜑𝑖 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑖 ) ) → ( 𝐹𝑛 ) ∈ 𝑆 )
52 38 39 44 45 51 measiuns ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑀 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹𝑛 ) ) = Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) )
53 3 ffnd ( 𝜑𝐹 Fn ℕ )
54 53 4 iuninc ( ( 𝜑𝑖 ∈ ℕ ) → 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹𝑛 ) = ( 𝐹𝑖 ) )
55 54 fveq2d ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑀 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝐹𝑛 ) ) = ( 𝑀 ‘ ( 𝐹𝑖 ) ) )
56 52 55 eqtr3d ( ( 𝜑𝑖 ∈ ℕ ) → Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) = ( 𝑀 ‘ ( 𝐹𝑖 ) ) )
57 56 mpteq2dva ( 𝜑 → ( 𝑖 ∈ ℕ ↦ Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( 𝑀 ‘ ( 𝐹𝑖 ) ) ) )
58 37 57 eqtr4d ( 𝜑 → ( 𝑀𝐹 ) = ( 𝑖 ∈ ℕ ↦ Σ* 𝑛 ∈ ( 1 ... 𝑖 ) ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) ) )
59 9 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹𝑛 ) ∈ 𝑆 )
60 dfiun2g ( ∀ 𝑛 ∈ ℕ ( 𝐹𝑛 ) ∈ 𝑆 𝑛 ∈ ℕ ( 𝐹𝑛 ) = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹𝑛 ) } )
61 59 60 syl ( 𝜑 𝑛 ∈ ℕ ( 𝐹𝑛 ) = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹𝑛 ) } )
62 fnrnfv ( 𝐹 Fn ℕ → ran 𝐹 = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹𝑛 ) } )
63 53 62 syl ( 𝜑 → ran 𝐹 = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹𝑛 ) } )
64 63 unieqd ( 𝜑 ran 𝐹 = { 𝑥 ∣ ∃ 𝑛 ∈ ℕ 𝑥 = ( 𝐹𝑛 ) } )
65 61 64 eqtr4d ( 𝜑 𝑛 ∈ ℕ ( 𝐹𝑛 ) = ran 𝐹 )
66 65 fveq2d ( 𝜑 → ( 𝑀 𝑛 ∈ ℕ ( 𝐹𝑛 ) ) = ( 𝑀 ran 𝐹 ) )
67 eqidd ( 𝜑 → ℕ = ℕ )
68 67 orcd ( 𝜑 → ( ℕ = ℕ ∨ ℕ = ( 1 ..^ ( 𝑖 + 1 ) ) ) )
69 38 39 68 2 9 measiuns ( 𝜑 → ( 𝑀 𝑛 ∈ ℕ ( 𝐹𝑛 ) ) = Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) )
70 66 69 eqtr3d ( 𝜑 → ( 𝑀 ran 𝐹 ) = Σ* 𝑛 ∈ ℕ ( 𝑀 ‘ ( ( 𝐹𝑛 ) ∖ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝐹𝑘 ) ) ) )
71 33 58 70 3brtr4d ( 𝜑 → ( 𝑀𝐹 ) ( ⇝𝑡𝐽 ) ( 𝑀 ran 𝐹 ) )