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	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℝ )
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 )

Metamath Proof Explorer

Theorem mbflimlem

Proof