smfliminf

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

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

Metamath Proof Explorer

Theorem smfliminf

Proof