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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑆 )
10 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝜑 )
11 fzossnn ⊢ ( 1 ..^ 𝑛 ) ⊆ ℕ
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑘 ∈ ( 1 ..^ 𝑛 ) )
13 11 12 sselid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑘 ∈ ℕ )
14 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
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 𝐹 ) )