smflim2

Description: The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). TODO: this has fewer distinct variable conditions than smflim and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflim2.n	$⊢ \underline{Ⅎ} m F$
	smflim2.x	$⊢ \underline{Ⅎ} x F$
	smflim2.m	$⊢ φ \to M \in ℤ$
	smflim2.z	$⊢ Z = ℤ_{\geq M}$
	smflim2.s	$⊢ φ \to S \in SAlg$
	smflim2.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflim2.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	smflim2.g	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
Assertion	smflim2	$⊢ φ \to G \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smflim2.n	$⊢ \underline{Ⅎ} m F$
2		smflim2.x	$⊢ \underline{Ⅎ} x F$
3		smflim2.m	$⊢ φ \to M \in ℤ$
4		smflim2.z	$⊢ Z = ℤ_{\geq M}$
5		smflim2.s	$⊢ φ \to S \in SAlg$
6		smflim2.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
7		smflim2.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
8		smflim2.g	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
9		nfcv	$⊢ \underline{Ⅎ} j F$
10		nfcv	$⊢ \underline{Ⅎ} y F$
11		nfcv	$⊢ \underline{Ⅎ} x Z$
12		nfcv	$⊢ \underline{Ⅎ} x ℤ_{\geq n}$
13		nfcv	$⊢ \underline{Ⅎ} x m$
14	2 13	nffv	$⊢ \underline{Ⅎ} x F (m)$
15	14	nfdm	$⊢ \underline{Ⅎ} x dom F (m)$
16	12 15	nfiin	$⊢ \underline{Ⅎ} x ⋂_{m \in ℤ_{\geq n}} dom F (m)$
17	11 16	nfiun	$⊢ \underline{Ⅎ} x ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
18		nfcv	$⊢ \underline{Ⅎ} y ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
19		nfv	$⊢ Ⅎ y (m \in Z ⟼ F (m) (x)) \in dom ⇝$
20		nfcv	$⊢ \underline{Ⅎ} j F (m) (y)$
21		nfcv	$⊢ \underline{Ⅎ} m j$
22	1 21	nffv	$⊢ \underline{Ⅎ} m F (j)$
23		nfcv	$⊢ \underline{Ⅎ} m y$
24	22 23	nffv	$⊢ \underline{Ⅎ} m F (j) (y)$
25		fveq2	$⊢ m = j \to F (m) = F (j)$
26	25	fveq1d	$⊢ m = j \to F (m) (y) = F (j) (y)$
27	20 24 26	cbvmpt	$⊢ (m \in Z ⟼ F (m) (y)) = (j \in Z ⟼ F (j) (y))$
28		nfcv	$⊢ \underline{Ⅎ} x j$
29	2 28	nffv	$⊢ \underline{Ⅎ} x F (j)$
30		nfcv	$⊢ \underline{Ⅎ} x y$
31	29 30	nffv	$⊢ \underline{Ⅎ} x F (j) (y)$
32	11 31	nfmpt	$⊢ \underline{Ⅎ} x (j \in Z ⟼ F (j) (y))$
33	27 32	nfcxfr	$⊢ \underline{Ⅎ} x (m \in Z ⟼ F (m) (y))$
34		nfcv	$⊢ \underline{Ⅎ} x dom ⇝$
35	33 34	nfel	$⊢ Ⅎ x (m \in Z ⟼ F (m) (y)) \in dom ⇝$
36		fveq2	$⊢ x = y \to F (m) (x) = F (m) (y)$
37	36	mpteq2dv	$⊢ x = y \to (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (y))$
38	37	eleq1d	$⊢ x = y \to ((m \in Z ⟼ F (m) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (y)) \in dom ⇝)$
39	17 18 19 35 38	cbvrabw	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} = \{y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (y)) \in dom ⇝\}$
40		fveq2	$⊢ n = k \to ℤ_{\geq n} = ℤ_{\geq k}$
41	40	iineq1d	$⊢ n = k \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{m \in ℤ_{\geq k}} dom F (m)$
42		nfcv	$⊢ \underline{Ⅎ} j dom F (m)$
43	22	nfdm	$⊢ \underline{Ⅎ} m dom F (j)$
44	25	dmeqd	$⊢ m = j \to dom F (m) = dom F (j)$
45	42 43 44	cbviin	$⊢ ⋂_{m \in ℤ_{\geq k}} dom F (m) = ⋂_{j \in ℤ_{\geq k}} dom F (j)$
46	45	a1i	$⊢ n = k \to ⋂_{m \in ℤ_{\geq k}} dom F (m) = ⋂_{j \in ℤ_{\geq k}} dom F (j)$
47	41 46	eqtrd	$⊢ n = k \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{j \in ℤ_{\geq k}} dom F (j)$
48	47	cbviunv	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{k \in Z} ⋂_{j \in ℤ_{\geq k}} dom F (j)$
49	48	eleq2i	$⊢ y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow y \in ⋃_{k \in Z} ⋂_{j \in ℤ_{\geq k}} dom F (j)$
50	27	eleq1i	$⊢ (m \in Z ⟼ F (m) (y)) \in dom ⇝ \leftrightarrow (j \in Z ⟼ F (j) (y)) \in dom ⇝$
51	49 50	anbi12i	$⊢ (y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land (m \in Z ⟼ F (m) (y)) \in dom ⇝) \leftrightarrow (y \in ⋃_{k \in Z} ⋂_{j \in ℤ_{\geq k}} dom F (j) \land (j \in Z ⟼ F (j) (y)) \in dom ⇝)$
52	51	rabbia2	$⊢ \{y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (y)) \in dom ⇝\} = \{y \in ⋃_{k \in Z} ⋂_{j \in ℤ_{\geq k}} dom F (j) \| (j \in Z ⟼ F (j) (y)) \in dom ⇝\}$
53	7 39 52	3eqtri	$⊢ D = \{y \in ⋃_{k \in Z} ⋂_{j \in ℤ_{\geq k}} dom F (j) \| (j \in Z ⟼ F (j) (y)) \in dom ⇝\}$
54		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
55	7 54	nfcxfr	$⊢ \underline{Ⅎ} x D$
56		nfcv	$⊢ \underline{Ⅎ} y D$
57		nfcv	$⊢ \underline{Ⅎ} y ⇝ ((m \in Z ⟼ F (m) (x)))$
58		nfcv	$⊢ \underline{Ⅎ} x ⇝$
59	58 32	nffv	$⊢ \underline{Ⅎ} x ⇝ ((j \in Z ⟼ F (j) (y)))$
60	27	a1i	$⊢ x = y \to (m \in Z ⟼ F (m) (y)) = (j \in Z ⟼ F (j) (y))$
61	37 60	eqtrd	$⊢ x = y \to (m \in Z ⟼ F (m) (x)) = (j \in Z ⟼ F (j) (y))$
62	61	fveq2d	$⊢ x = y \to ⇝ ((m \in Z ⟼ F (m) (x))) = ⇝ ((j \in Z ⟼ F (j) (y)))$
63	55 56 57 59 62	cbvmptf	$⊢ (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x)))) = (y \in D ⟼ ⇝ ((j \in Z ⟼ F (j) (y))))$
64	8 63	eqtri	$⊢ G = (y \in D ⟼ ⇝ ((j \in Z ⟼ F (j) (y))))$
65	9 10 3 4 5 6 53 64	smflim	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smflim2

Proof