Metamath Proof Explorer

Theorem mbflimlem

Description: The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbflim.1 ⊢ Z = ℤ ≥ M
mbflim.2 ⊢ φ → M ∈ ℤ
mbflim.4 ⊢ φ ∧ x ∈ A → n ∈ Z ⟼ B ⇝ C
mbflim.5 ⊢ φ ∧ n ∈ Z → x ∈ A ⟼ B ∈ MblFn
mbflimlem.6 ⊢ φ ∧ n ∈ Z ∧ x ∈ A → B ∈ ℝ
Assertion mbflimlem ⊢ φ → x ∈ A ⟼ C ∈ MblFn

Proof

Step Hyp Ref Expression
1 mbflim.1 ⊢ Z = ℤ ≥ M
2 mbflim.2 ⊢ φ → M ∈ ℤ
3 mbflim.4 ⊢ φ ∧ x ∈ A → n ∈ Z ⟼ B ⇝ C
4 mbflim.5 ⊢ φ ∧ n ∈ Z → x ∈ A ⟼ B ∈ MblFn
5 mbflimlem.6 ⊢ φ ∧ n ∈ Z ∧ x ∈ A → B ∈ ℝ
6 5 anass1rs ⊢ φ ∧ x ∈ A ∧ n ∈ Z → B ∈ ℝ
7 6 fmpttd ⊢ φ ∧ x ∈ A → n ∈ Z ⟼ B : Z ⟶ ℝ
8 2 adantr ⊢ φ ∧ x ∈ A → M ∈ ℤ
9 climrel ⊢ Rel ⁡ ⇝
10 9 releldmi ⊢ n ∈ Z ⟼ B ⇝ C → n ∈ Z ⟼ B ∈ dom ⁡ ⇝
11 3 10 syl ⊢ φ ∧ x ∈ A → n ∈ Z ⟼ B ∈ dom ⁡ ⇝
12 1 climcau ⊢ M ∈ ℤ ∧ n ∈ Z ⟼ B ∈ dom ⁡ ⇝ → ∀ y ∈ ℝ + ∃ k ∈ Z ∀ j ∈ ℤ ≥ k n ∈ Z ⟼ B ⁡ j − n ∈ Z ⟼ B ⁡ k < y
13 8 11 12 syl2anc ⊢ φ ∧ x ∈ A → ∀ y ∈ ℝ + ∃ k ∈ Z ∀ j ∈ ℤ ≥ k n ∈ Z ⟼ B ⁡ j − n ∈ Z ⟼ B ⁡ k < y
14 1 7 13 caurcvg ⊢ φ ∧ x ∈ A → n ∈ Z ⟼ B ⇝ lim sup ⁡ n ∈ Z ⟼ B
15 climuni ⊢ n ∈ Z ⟼ B ⇝ lim sup ⁡ n ∈ Z ⟼ B ∧ n ∈ Z ⟼ B ⇝ C → lim sup ⁡ n ∈ Z ⟼ B = C
16 14 3 15 syl2anc ⊢ φ ∧ x ∈ A → lim sup ⁡ n ∈ Z ⟼ B = C
17 16 mpteq2dva ⊢ φ → x ∈ A ⟼ lim sup ⁡ n ∈ Z ⟼ B = x ∈ A ⟼ C
18 eqid ⊢ x ∈ A ⟼ lim sup ⁡ n ∈ Z ⟼ B = x ∈ A ⟼ lim sup ⁡ n ∈ Z ⟼ B
19 eqid ⊢ m ∈ ℝ ⟼ sup n ∈ Z ⟼ B m +∞ ∩ ℝ * ℝ * < = m ∈ ℝ ⟼ sup n ∈ Z ⟼ B m +∞ ∩ ℝ * ℝ * <
20 7 ffvelcdmda ⊢ φ ∧ x ∈ A ∧ k ∈ Z → n ∈ Z ⟼ B ⁡ k ∈ ℝ
21 1 8 14 20 climrecl ⊢ φ ∧ x ∈ A → lim sup ⁡ n ∈ Z ⟼ B ∈ ℝ
22 1 18 19 2 21 4 5 mbflimsup ⊢ φ → x ∈ A ⟼ lim sup ⁡ n ∈ Z ⟼ B ∈ MblFn
23 17 22 eqeltrrd ⊢ φ → x ∈ A ⟼ C ∈ MblFn