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∈ℤ≥kn∈Z⟼B⁡j−n∈Z⟼B⁡k<y
13 8 11 12 syl2anc ⊢φ∧x∈A→∀y∈ℝ+∃k∈Z∀j∈ℤ≥kn∈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∈ℝ⟼supn∈Z⟼Bm+∞∩ℝ*ℝ*<=m∈ℝ⟼supn∈Z⟼Bm+∞∩ℝ*ℝ*<
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