Metamath Proof Explorer

Theorem mbflim

Description: The pointwise limit of a sequence of measurable 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
mbflim.6 ⊢φ∧n∈Z∧x∈A→B∈V
Assertion mbflim ⊢φ→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 mbflim.6 ⊢φ∧n∈Z∧x∈A→B∈V
6 1 fvexi ⊢Z∈V
7 6 mptex ⊢n∈Z⟼ℜ⁡B∈V
8 7 a1i ⊢φ∧x∈A→n∈Z⟼ℜ⁡B∈V
9 2 adantr ⊢φ∧x∈A→M∈ℤ
10 5 anassrs ⊢φ∧n∈Z∧x∈A→B∈V
11 4 10 mbfmptcl ⊢φ∧n∈Z∧x∈A→B∈ℂ
12 11 an32s ⊢φ∧x∈A∧n∈Z→B∈ℂ
13 12 fmpttd ⊢φ∧x∈A→n∈Z⟼B:Z⟶ℂ
14 13 ffvelcdmda ⊢φ∧x∈A∧k∈Z→n∈Z⟼B⁡k∈ℂ
15 simpr ⊢φ∧x∈A∧n∈Z→n∈Z
16 12 recld ⊢φ∧x∈A∧n∈Z→ℜ⁡B∈ℝ
17 eqid ⊢n∈Z⟼ℜ⁡B=n∈Z⟼ℜ⁡B
18 17 fvmpt2 ⊢n∈Z∧ℜ⁡B∈ℝ→n∈Z⟼ℜ⁡B⁡n=ℜ⁡B
19 15 16 18 syl2anc ⊢φ∧x∈A∧n∈Z→n∈Z⟼ℜ⁡B⁡n=ℜ⁡B
20 eqid ⊢n∈Z⟼B=n∈Z⟼B
21 20 fvmpt2 ⊢n∈Z∧B∈ℂ→n∈Z⟼B⁡n=B
22 15 12 21 syl2anc ⊢φ∧x∈A∧n∈Z→n∈Z⟼B⁡n=B
23 22 fveq2d ⊢φ∧x∈A∧n∈Z→ℜ⁡n∈Z⟼B⁡n=ℜ⁡B
24 19 23 eqtr4d ⊢φ∧x∈A∧n∈Z→n∈Z⟼ℜ⁡B⁡n=ℜ⁡n∈Z⟼B⁡n
25 24 ralrimiva ⊢φ∧x∈A→∀n∈Zn∈Z⟼ℜ⁡B⁡n=ℜ⁡n∈Z⟼B⁡n
26 nffvmpt1 ⊢Ⅎ_nn∈Z⟼ℜ⁡B⁡k
27 nfcv ⊢Ⅎ_nℜ
28 nffvmpt1 ⊢Ⅎ_nn∈Z⟼B⁡k
29 27 28 nffv ⊢Ⅎ_nℜ⁡n∈Z⟼B⁡k
30 26 29 nfeq ⊢Ⅎnn∈Z⟼ℜ⁡B⁡k=ℜ⁡n∈Z⟼B⁡k
31 nfv ⊢Ⅎkn∈Z⟼ℜ⁡B⁡n=ℜ⁡n∈Z⟼B⁡n
32 fveq2 ⊢k=n→n∈Z⟼ℜ⁡B⁡k=n∈Z⟼ℜ⁡B⁡n
33 2fveq3 ⊢k=n→ℜ⁡n∈Z⟼B⁡k=ℜ⁡n∈Z⟼B⁡n
34 32 33 eqeq12d ⊢k=n→n∈Z⟼ℜ⁡B⁡k=ℜ⁡n∈Z⟼B⁡k↔n∈Z⟼ℜ⁡B⁡n=ℜ⁡n∈Z⟼B⁡n
35 30 31 34 cbvralw ⊢∀k∈Zn∈Z⟼ℜ⁡B⁡k=ℜ⁡n∈Z⟼B⁡k↔∀n∈Zn∈Z⟼ℜ⁡B⁡n=ℜ⁡n∈Z⟼B⁡n
36 25 35 sylibr ⊢φ∧x∈A→∀k∈Zn∈Z⟼ℜ⁡B⁡k=ℜ⁡n∈Z⟼B⁡k
37 36 r19.21bi ⊢φ∧x∈A∧k∈Z→n∈Z⟼ℜ⁡B⁡k=ℜ⁡n∈Z⟼B⁡k
38 1 3 8 9 14 37 climre ⊢φ∧x∈A→n∈Z⟼ℜ⁡B⇝ℜ⁡C
39 11 ismbfcn2 ⊢φ∧n∈Z→x∈A⟼B∈MblFn↔x∈A⟼ℜ⁡B∈MblFn∧x∈A⟼ℑ⁡B∈MblFn
40 4 39 mpbid ⊢φ∧n∈Z→x∈A⟼ℜ⁡B∈MblFn∧x∈A⟼ℑ⁡B∈MblFn
41 40 simpld ⊢φ∧n∈Z→x∈A⟼ℜ⁡B∈MblFn
42 11 anasss ⊢φ∧n∈Z∧x∈A→B∈ℂ
43 42 recld ⊢φ∧n∈Z∧x∈A→ℜ⁡B∈ℝ
44 1 2 38 41 43 mbflimlem ⊢φ→x∈A⟼ℜ⁡C∈MblFn
45 6 mptex ⊢n∈Z⟼ℑ⁡B∈V
46 45 a1i ⊢φ∧x∈A→n∈Z⟼ℑ⁡B∈V
47 12 imcld ⊢φ∧x∈A∧n∈Z→ℑ⁡B∈ℝ
48 eqid ⊢n∈Z⟼ℑ⁡B=n∈Z⟼ℑ⁡B
49 48 fvmpt2 ⊢n∈Z∧ℑ⁡B∈ℝ→n∈Z⟼ℑ⁡B⁡n=ℑ⁡B
50 15 47 49 syl2anc ⊢φ∧x∈A∧n∈Z→n∈Z⟼ℑ⁡B⁡n=ℑ⁡B
51 22 fveq2d ⊢φ∧x∈A∧n∈Z→ℑ⁡n∈Z⟼B⁡n=ℑ⁡B
52 50 51 eqtr4d ⊢φ∧x∈A∧n∈Z→n∈Z⟼ℑ⁡B⁡n=ℑ⁡n∈Z⟼B⁡n
53 52 ralrimiva ⊢φ∧x∈A→∀n∈Zn∈Z⟼ℑ⁡B⁡n=ℑ⁡n∈Z⟼B⁡n
54 nffvmpt1 ⊢Ⅎ_nn∈Z⟼ℑ⁡B⁡k
55 nfcv ⊢Ⅎ_nℑ
56 55 28 nffv ⊢Ⅎ_nℑ⁡n∈Z⟼B⁡k
57 54 56 nfeq ⊢Ⅎnn∈Z⟼ℑ⁡B⁡k=ℑ⁡n∈Z⟼B⁡k
58 nfv ⊢Ⅎkn∈Z⟼ℑ⁡B⁡n=ℑ⁡n∈Z⟼B⁡n
59 fveq2 ⊢k=n→n∈Z⟼ℑ⁡B⁡k=n∈Z⟼ℑ⁡B⁡n
60 2fveq3 ⊢k=n→ℑ⁡n∈Z⟼B⁡k=ℑ⁡n∈Z⟼B⁡n
61 59 60 eqeq12d ⊢k=n→n∈Z⟼ℑ⁡B⁡k=ℑ⁡n∈Z⟼B⁡k↔n∈Z⟼ℑ⁡B⁡n=ℑ⁡n∈Z⟼B⁡n
62 57 58 61 cbvralw ⊢∀k∈Zn∈Z⟼ℑ⁡B⁡k=ℑ⁡n∈Z⟼B⁡k↔∀n∈Zn∈Z⟼ℑ⁡B⁡n=ℑ⁡n∈Z⟼B⁡n
63 53 62 sylibr ⊢φ∧x∈A→∀k∈Zn∈Z⟼ℑ⁡B⁡k=ℑ⁡n∈Z⟼B⁡k
64 63 r19.21bi ⊢φ∧x∈A∧k∈Z→n∈Z⟼ℑ⁡B⁡k=ℑ⁡n∈Z⟼B⁡k
65 1 3 46 9 14 64 climim ⊢φ∧x∈A→n∈Z⟼ℑ⁡B⇝ℑ⁡C
66 40 simprd ⊢φ∧n∈Z→x∈A⟼ℑ⁡B∈MblFn
67 42 imcld ⊢φ∧n∈Z∧x∈A→ℑ⁡B∈ℝ
68 1 2 65 66 67 mbflimlem ⊢φ→x∈A⟼ℑ⁡C∈MblFn
69 climcl ⊢n∈Z⟼B⇝C→C∈ℂ
70 3 69 syl ⊢φ∧x∈A→C∈ℂ
71 70 ismbfcn2 ⊢φ→x∈A⟼C∈MblFn↔x∈A⟼ℜ⁡C∈MblFn∧x∈A⟼ℑ⁡C∈MblFn
72 44 68 71 mpbir2and ⊢φ→x∈A⟼C∈MblFn