This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
mbflim.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
mbflim.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐶 )
mbflim.5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
mbflimlem.6 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ )
Assertion mbflimlem ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbflim.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 mbflim.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 mbflim.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐶 )
4 mbflim.5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5 mbflimlem.6 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ )
6 5 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
7 6 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ℤ )
9 climrel ⊢ Rel ⇝
10 9 releldmi ⊢ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐶 → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ )
11 3 10 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ )
12 1 climcau ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ∈ dom ⇝ ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) − ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) ) < 𝑦 )
13 8 11 12 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) − ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) ) < 𝑦 )
14 1 7 13 caurcvg ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) )
15 climuni ⊢ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ∧ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐶 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) = 𝐶 )
16 14 3 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) = 𝐶 )
17 16 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
18 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) )
19 eqid ⊢ ( 𝑚 ∈ ℝ ↦ sup ( ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) “ ( 𝑚 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑚 ∈ ℝ ↦ sup ( ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) “ ( 𝑚 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
20 7 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
21 1 8 14 20 climrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ )
22 1 18 19 2 21 4 5 mbflimsup ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ) ∈ MblFn )
23 17 22 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )