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 = ℤ_{\geq M}$
	mbflim.2	$⊢ φ \to M \in ℤ$
	mbflim.4	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) ⇝ C$
	mbflim.5	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in MblFn$
	mbflim.6	$⊢ (φ \land (n \in Z \land x \in A)) \to B \in V$
Assertion	mbflim	$⊢ φ \to (x \in A ⟼ C) \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbflim.1	$⊢ Z = ℤ_{\geq M}$
2		mbflim.2	$⊢ φ \to M \in ℤ$
3		mbflim.4	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) ⇝ C$
4		mbflim.5	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in MblFn$
5		mbflim.6	$⊢ (φ \land (n \in Z \land x \in A)) \to B \in V$
6	1	fvexi	$⊢ Z \in V$
7	6	mptex	$⊢ (n \in Z ⟼ ℜ (B)) \in V$
8	7	a1i	$⊢ (φ \land x \in A) \to (n \in Z ⟼ ℜ (B)) \in V$
9	2	adantr	$⊢ (φ \land x \in A) \to M \in ℤ$
10	5	anassrs	$⊢ ((φ \land n \in Z) \land x \in A) \to B \in V$
11	4 10	mbfmptcl	$⊢ ((φ \land n \in Z) \land x \in A) \to B \in ℂ$
12	11	an32s	$⊢ ((φ \land x \in A) \land n \in Z) \to B \in ℂ$
13	12	fmpttd	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) : Z ⟶ ℂ$
14	13	ffvelrnda	$⊢ ((φ \land x \in A) \land k \in Z) \to (n \in Z ⟼ B) (k) \in ℂ$
15		simpr	$⊢ ((φ \land x \in A) \land n \in Z) \to n \in Z$
16	12	recld	$⊢ ((φ \land x \in A) \land n \in Z) \to ℜ (B) \in ℝ$
17		eqid	$⊢ (n \in Z ⟼ ℜ (B)) = (n \in Z ⟼ ℜ (B))$
18	17	fvmpt2	$⊢ (n \in Z \land ℜ (B) \in ℝ) \to (n \in Z ⟼ ℜ (B)) (n) = ℜ (B)$
19	15 16 18	syl2anc	$⊢ ((φ \land x \in A) \land n \in Z) \to (n \in Z ⟼ ℜ (B)) (n) = ℜ (B)$
20		eqid	$⊢ (n \in Z ⟼ B) = (n \in Z ⟼ B)$
21	20	fvmpt2	$⊢ (n \in Z \land B \in ℂ) \to (n \in Z ⟼ B) (n) = B$
22	15 12 21	syl2anc	$⊢ ((φ \land x \in A) \land n \in Z) \to (n \in Z ⟼ B) (n) = B$
23	22	fveq2d	$⊢ ((φ \land x \in A) \land n \in Z) \to ℜ ((n \in Z ⟼ B) (n)) = ℜ (B)$
24	19 23	eqtr4d	$⊢ ((φ \land x \in A) \land n \in Z) \to (n \in Z ⟼ ℜ (B)) (n) = ℜ ((n \in Z ⟼ B) (n))$
25	24	ralrimiva	$⊢ (φ \land x \in A) \to \forall n \in Z (n \in Z ⟼ ℜ (B)) (n) = ℜ ((n \in Z ⟼ B) (n))$
26		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ ℜ (B)) (k)$
27		nfcv	$⊢ \underline{Ⅎ} n ℜ$
28		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ B) (k)$
29	27 28	nffv	$⊢ \underline{Ⅎ} n ℜ ((n \in Z ⟼ B) (k))$
30	26 29	nfeq	$⊢ Ⅎ n (n \in Z ⟼ ℜ (B)) (k) = ℜ ((n \in Z ⟼ B) (k))$
31		nfv	$⊢ Ⅎ k (n \in Z ⟼ ℜ (B)) (n) = ℜ ((n \in Z ⟼ B) (n))$
32		fveq2	$⊢ k = n \to (n \in Z ⟼ ℜ (B)) (k) = (n \in Z ⟼ ℜ (B)) (n)$
33		2fveq3	$⊢ k = n \to ℜ ((n \in Z ⟼ B) (k)) = ℜ ((n \in Z ⟼ B) (n))$
34	32 33	eqeq12d	$⊢ k = n \to ((n \in Z ⟼ ℜ (B)) (k) = ℜ ((n \in Z ⟼ B) (k)) \leftrightarrow (n \in Z ⟼ ℜ (B)) (n) = ℜ ((n \in Z ⟼ B) (n)))$
35	30 31 34	cbvralw	$⊢ \forall k \in Z (n \in Z ⟼ ℜ (B)) (k) = ℜ ((n \in Z ⟼ B) (k)) \leftrightarrow \forall n \in Z (n \in Z ⟼ ℜ (B)) (n) = ℜ ((n \in Z ⟼ B) (n))$
36	25 35	sylibr	$⊢ (φ \land x \in A) \to \forall k \in Z (n \in Z ⟼ ℜ (B)) (k) = ℜ ((n \in Z ⟼ B) (k))$
37	36	r19.21bi	$⊢ ((φ \land x \in A) \land k \in Z) \to (n \in Z ⟼ ℜ (B)) (k) = ℜ ((n \in Z ⟼ B) (k))$
38	1 3 8 9 14 37	climre	$⊢ (φ \land x \in A) \to (n \in Z ⟼ ℜ (B)) ⇝ ℜ (C)$
39	11	ismbfcn2	$⊢ (φ \land n \in Z) \to ((x \in A ⟼ B) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn))$
40	4 39	mpbid	$⊢ (φ \land n \in Z) \to ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn)$
41	40	simpld	$⊢ (φ \land n \in Z) \to (x \in A ⟼ ℜ (B)) \in MblFn$
42	11	anasss	$⊢ (φ \land (n \in Z \land x \in A)) \to B \in ℂ$
43	42	recld	$⊢ (φ \land (n \in Z \land x \in A)) \to ℜ (B) \in ℝ$
44	1 2 38 41 43	mbflimlem	$⊢ φ \to (x \in A ⟼ ℜ (C)) \in MblFn$
45	6	mptex	$⊢ (n \in Z ⟼ ℑ (B)) \in V$
46	45	a1i	$⊢ (φ \land x \in A) \to (n \in Z ⟼ ℑ (B)) \in V$
47	12	imcld	$⊢ ((φ \land x \in A) \land n \in Z) \to ℑ (B) \in ℝ$
48		eqid	$⊢ (n \in Z ⟼ ℑ (B)) = (n \in Z ⟼ ℑ (B))$
49	48	fvmpt2	$⊢ (n \in Z \land ℑ (B) \in ℝ) \to (n \in Z ⟼ ℑ (B)) (n) = ℑ (B)$
50	15 47 49	syl2anc	$⊢ ((φ \land x \in A) \land n \in Z) \to (n \in Z ⟼ ℑ (B)) (n) = ℑ (B)$
51	22	fveq2d	$⊢ ((φ \land x \in A) \land n \in Z) \to ℑ ((n \in Z ⟼ B) (n)) = ℑ (B)$
52	50 51	eqtr4d	$⊢ ((φ \land x \in A) \land n \in Z) \to (n \in Z ⟼ ℑ (B)) (n) = ℑ ((n \in Z ⟼ B) (n))$
53	52	ralrimiva	$⊢ (φ \land x \in A) \to \forall n \in Z (n \in Z ⟼ ℑ (B)) (n) = ℑ ((n \in Z ⟼ B) (n))$
54		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ ℑ (B)) (k)$
55		nfcv	$⊢ \underline{Ⅎ} n ℑ$
56	55 28	nffv	$⊢ \underline{Ⅎ} n ℑ ((n \in Z ⟼ B) (k))$
57	54 56	nfeq	$⊢ Ⅎ n (n \in Z ⟼ ℑ (B)) (k) = ℑ ((n \in Z ⟼ B) (k))$
58		nfv	$⊢ Ⅎ k (n \in Z ⟼ ℑ (B)) (n) = ℑ ((n \in Z ⟼ B) (n))$
59		fveq2	$⊢ k = n \to (n \in Z ⟼ ℑ (B)) (k) = (n \in Z ⟼ ℑ (B)) (n)$
60		2fveq3	$⊢ k = n \to ℑ ((n \in Z ⟼ B) (k)) = ℑ ((n \in Z ⟼ B) (n))$
61	59 60	eqeq12d	$⊢ k = n \to ((n \in Z ⟼ ℑ (B)) (k) = ℑ ((n \in Z ⟼ B) (k)) \leftrightarrow (n \in Z ⟼ ℑ (B)) (n) = ℑ ((n \in Z ⟼ B) (n)))$
62	57 58 61	cbvralw	$⊢ \forall k \in Z (n \in Z ⟼ ℑ (B)) (k) = ℑ ((n \in Z ⟼ B) (k)) \leftrightarrow \forall n \in Z (n \in Z ⟼ ℑ (B)) (n) = ℑ ((n \in Z ⟼ B) (n))$
63	53 62	sylibr	$⊢ (φ \land x \in A) \to \forall k \in Z (n \in Z ⟼ ℑ (B)) (k) = ℑ ((n \in Z ⟼ B) (k))$
64	63	r19.21bi	$⊢ ((φ \land x \in A) \land k \in Z) \to (n \in Z ⟼ ℑ (B)) (k) = ℑ ((n \in Z ⟼ B) (k))$
65	1 3 46 9 14 64	climim	$⊢ (φ \land x \in A) \to (n \in Z ⟼ ℑ (B)) ⇝ ℑ (C)$
66	40	simprd	$⊢ (φ \land n \in Z) \to (x \in A ⟼ ℑ (B)) \in MblFn$
67	42	imcld	$⊢ (φ \land (n \in Z \land x \in A)) \to ℑ (B) \in ℝ$
68	1 2 65 66 67	mbflimlem	$⊢ φ \to (x \in A ⟼ ℑ (C)) \in MblFn$
69		climcl	$⊢ (n \in Z ⟼ B) ⇝ C \to C \in ℂ$
70	3 69	syl	$⊢ (φ \land x \in A) \to C \in ℂ$
71	70	ismbfcn2	$⊢ φ \to ((x \in A ⟼ C) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (C)) \in MblFn \land (x \in A ⟼ ℑ (C)) \in MblFn))$
72	44 68 71	mpbir2and	$⊢ φ \to (x \in A ⟼ C) \in MblFn$

Metamath Proof Explorer

Theorem mbflim

Proof