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

Metamath Proof Explorer

Theorem mbfulm

Description: A uniform limit of measurable functions is measurable. (This is just a corollary of the fact that a pointwise limit of measurable functions is measurable, see mbflim .) (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses mbfulm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
mbfulm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
mbfulm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ MblFn )
mbfulm.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
Assertion mbfulm ( 𝜑 → 𝐺 ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfulm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 mbfulm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 mbfulm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ MblFn )
4 mbfulm.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
5 ulmcl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
6 4 5 syl ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
7 6 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑧 ) ) )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑀 ∈ ℤ )
9 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
10 ulmf2 ⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
11 9 4 10 syl2anc ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
14 1 fvexi ⊢ 𝑍 ∈ V
15 14 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ V
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ V )
17 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
18 17 fveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) )
19 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
20 fvex ⊢ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ∈ V
21 18 19 20 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) )
22 21 eqcomd ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
24 4 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
25 1 8 12 13 16 23 24 ulmclm ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
26 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
27 elmapi ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
29 28 feqmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝑧 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
30 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ MblFn )
31 29 30 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑧 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ MblFn )
32 28 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
33 32 anasss ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
34 1 2 25 31 33 mbflim ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ MblFn )
35 7 34 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ MblFn )