smfliminflem

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	smfliminflem.m	$⊢ φ \to M \in ℤ$
	smfliminflem.z	$⊢ Z = ℤ_{\geq M}$
	smfliminflem.s	$⊢ φ \to S \in SAlg$
	smfliminflem.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smfliminflem.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
	smfliminflem.g	$⊢ G = (x \in D ⟼ lim inf ((m \in Z ⟼ F (m) (x))))$
Assertion	smfliminflem	$⊢ φ \to G \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfliminflem.m	$⊢ φ \to M \in ℤ$
2		smfliminflem.z	$⊢ Z = ℤ_{\geq M}$
3		smfliminflem.s	$⊢ φ \to S \in SAlg$
4		smfliminflem.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smfliminflem.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
6		smfliminflem.g	$⊢ G = (x \in D ⟼ lim inf ((m \in Z ⟼ F (m) (x))))$
7	6	a1i	$⊢ φ \to G = (x \in D ⟼ lim inf ((m \in Z ⟼ F (m) (x))))$
8		ssrab2	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ\} \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
9	5 8	eqsstri	$⊢ D \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
10		id	$⊢ x \in D \to x \in D$
11	9 10	sseldi	$⊢ x \in D \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
12		eqid	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
13	2 12	allbutfi	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow \exists n \in Z \forall m \in ℤ_{\geq n} x \in dom F (m)$
14	11 13	sylib	$⊢ x \in D \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in dom F (m)$
15	14	adantl	$⊢ (φ \land x \in D) \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in dom F (m)$
16		nfv	$⊢ Ⅎ m (φ \land n \in Z)$
17		nfra1	$⊢ Ⅎ m \forall m \in ℤ_{\geq n} x \in dom F (m)$
18	16 17	nfan	$⊢ Ⅎ m ((φ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in dom F (m))$
19	2	fvexi	$⊢ Z \in V$
20	19	a1i	$⊢ ((φ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \to Z \in V$
21	2	eluzelz2	$⊢ n \in Z \to n \in ℤ$
22	21	zred	$⊢ n \in Z \to n \in ℝ$
23	22	ad2antlr	$⊢ ((φ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \to n \in ℝ$
24		simpll	$⊢ ((φ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \to φ$
25		elinel1	$⊢ m \in (Z \cap [n, +∞)) \to m \in Z$
26	3	adantr	$⊢ (φ \land m \in Z) \to S \in SAlg$
27	4	ffvelrnda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
28		eqid	$⊢ dom F (m) = dom F (m)$
29	26 27 28	smff	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
30	24 25 29	syl2an	$⊢ (((φ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \land m \in (Z \cap [n, +∞))) \to F (m) : dom F (m) ⟶ ℝ$
31		simplr	$⊢ ((n \in Z \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \land m \in (Z \cap [n, +∞))) \to \forall m \in ℤ_{\geq n} x \in dom F (m)$
32		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
33	21	adantr	$⊢ (n \in Z \land m \in (Z \cap [n, +∞))) \to n \in ℤ$
34	2 25	eluzelz2d	$⊢ m \in (Z \cap [n, +∞)) \to m \in ℤ$
35	34	adantl	$⊢ (n \in Z \land m \in (Z \cap [n, +∞))) \to m \in ℤ$
36	22	rexrd	$⊢ n \in Z \to n \in ℝ^{*}$
37	36	adantr	$⊢ (n \in Z \land m \in (Z \cap [n, +∞))) \to n \in ℝ^{*}$
38		pnfxr	$⊢ +∞ \in ℝ^{*}$
39	38	a1i	$⊢ (n \in Z \land m \in (Z \cap [n, +∞))) \to +∞ \in ℝ^{*}$
40		elinel2	$⊢ m \in (Z \cap [n, +∞)) \to m \in [n, +∞)$
41	40	adantl	$⊢ (n \in Z \land m \in (Z \cap [n, +∞))) \to m \in [n, +∞)$
42	37 39 41	icogelbd	$⊢ (n \in Z \land m \in (Z \cap [n, +∞))) \to n \leq m$
43	32 33 35 42	eluzd	$⊢ (n \in Z \land m \in (Z \cap [n, +∞))) \to m \in ℤ_{\geq n}$
44	43	adantlr	$⊢ ((n \in Z \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \land m \in (Z \cap [n, +∞))) \to m \in ℤ_{\geq n}$
45		rspa	$⊢ (\forall m \in ℤ_{\geq n} x \in dom F (m) \land m \in ℤ_{\geq n}) \to x \in dom F (m)$
46	31 44 45	syl2anc	$⊢ ((n \in Z \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \land m \in (Z \cap [n, +∞))) \to x \in dom F (m)$
47	46	adantlll	$⊢ (((φ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \land m \in (Z \cap [n, +∞))) \to x \in dom F (m)$
48	30 47	ffvelrnd	$⊢ (((φ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \land m \in (Z \cap [n, +∞))) \to F (m) (x) \in ℝ$
49	18 20 23 48	liminfval4	$⊢ ((φ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in dom F (m)) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x)))$
50	49	rexlimdva2	$⊢ φ \to (\exists n \in Z \forall m \in ℤ_{\geq n} x \in dom F (m) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))))$
51	50	adantr	$⊢ (φ \land x \in D) \to (\exists n \in Z \forall m \in ℤ_{\geq n} x \in dom F (m) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))))$
52	15 51	mpd	$⊢ (φ \land x \in D) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x)))$
53	52	xnegeqd	$⊢ (φ \land x \in D) \to - lim inf ((m \in Z ⟼ F (m) (x))) = - (- lim sup ((m \in Z ⟼ - F (m) (x))))$
54	19	mptex	$⊢ (m \in Z ⟼ - F (m) (x)) \in V$
55	54	limsupcli	$⊢ lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ^{*}$
56	55	xnegnegi	$⊢ - (- lim sup ((m \in Z ⟼ - F (m) (x)))) = lim sup ((m \in Z ⟼ - F (m) (x)))$
57	56	a1i	$⊢ (φ \land x \in D) \to - (- lim sup ((m \in Z ⟼ - F (m) (x)))) = lim sup ((m \in Z ⟼ - F (m) (x)))$
58	53 57	eqtr2d	$⊢ (φ \land x \in D) \to lim sup ((m \in Z ⟼ - F (m) (x))) = - lim inf ((m \in Z ⟼ F (m) (x)))$
59	5	rabeq2i	$⊢ x \in D \leftrightarrow (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ)$
60	59	simprbi	$⊢ x \in D \to lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ$
61	60	adantl	$⊢ (φ \land x \in D) \to lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ$
62	61	rexnegd	$⊢ (φ \land x \in D) \to - lim inf ((m \in Z ⟼ F (m) (x))) = - lim inf ((m \in Z ⟼ F (m) (x)))$
63	58 62	eqtr2d	$⊢ (φ \land x \in D) \to - lim inf ((m \in Z ⟼ F (m) (x))) = lim sup ((m \in Z ⟼ - F (m) (x)))$
64	61	renegcld	$⊢ (φ \land x \in D) \to - lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ$
65	63 64	eqeltrrd	$⊢ (φ \land x \in D) \to lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ$
66	65	rexnegd	$⊢ (φ \land x \in D) \to - lim sup ((m \in Z ⟼ - F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x)))$
67	52 66	eqtrd	$⊢ (φ \land x \in D) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x)))$
68	67	mpteq2dva	$⊢ φ \to (x \in D ⟼ lim inf ((m \in Z ⟼ F (m) (x)))) = (x \in D ⟼ - lim sup ((m \in Z ⟼ - F (m) (x))))$
69	7 68	eqtrd	$⊢ φ \to G = (x \in D ⟼ - lim sup ((m \in Z ⟼ - F (m) (x))))$
70		nfv	$⊢ Ⅎ x φ$
71	21 32	uzn0d	$⊢ n \in Z \to ℤ_{\geq n} \neq \emptyset$
72		fvex	$⊢ F (m) \in V$
73	72	dmex	$⊢ dom F (m) \in V$
74	73	rgenw	$⊢ \forall m \in ℤ_{\geq n} dom F (m) \in V$
75	74	a1i	$⊢ n \in Z \to \forall m \in ℤ_{\geq n} dom F (m) \in V$
76		iinexg	$⊢ (ℤ_{\geq n} \neq \emptyset \land \forall m \in ℤ_{\geq n} dom F (m) \in V) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
77	71 75 76	syl2anc	$⊢ n \in Z \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
78	77	rgen	$⊢ \forall n \in Z ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
79		iunexg	$⊢ (Z \in V \land \forall n \in Z ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V) \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
80	19 78 79	mp2an	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
81	80 9	ssexi	$⊢ D \in V$
82	81	a1i	$⊢ φ \to D \in V$
83	5	a1i	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
84	13	biimpi	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in dom F (m)$
85	50	imp	$⊢ (φ \land \exists n \in Z \forall m \in ℤ_{\geq n} x \in dom F (m)) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x)))$
86	84 85	sylan2	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x)))$
87	55	a1i	$⊢ (lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \land lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ) \to lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ^{*}$
88		simpl	$⊢ (lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \land lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x)))$
89		simpr	$⊢ (lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \land lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ) \to lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ$
90	88 89	eqeltrrd	$⊢ (lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \land lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ) \to - lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ$
91		xnegrecl2	$⊢ (lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ^{*} \land - lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ) \to lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ$
92	87 90 91	syl2anc	$⊢ (lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \land lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ) \to lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ$
93		simpl	$⊢ (lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \land lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ) \to lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x)))$
94		xnegrecl	$⊢ lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ \to - lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ$
95	94	adantl	$⊢ (lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \land lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ) \to - lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ$
96	93 95	eqeltrd	$⊢ (lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \land lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ) \to lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ$
97	92 96	impbida	$⊢ lim inf ((m \in Z ⟼ F (m) (x))) = - lim sup ((m \in Z ⟼ - F (m) (x))) \to (lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ \leftrightarrow lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ)$
98	86 97	syl	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to (lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ \leftrightarrow lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ)$
99	98	rabbidva	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim inf ((m \in Z ⟼ F (m) (x))) \in ℝ\} = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ\}$
100	83 99	eqtrd	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ\}$
101	70 100	mpteq1df	$⊢ φ \to (x \in D ⟼ lim sup ((m \in Z ⟼ - F (m) (x)))) = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ\} ⟼ lim sup ((m \in Z ⟼ - F (m) (x))))$
102		nfv	$⊢ Ⅎ m φ$
103		nfv	$⊢ Ⅎ n φ$
104		negex	$⊢ - F (m) (x) \in V$
105	104	a1i	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to - F (m) (x) \in V$
106		nfv	$⊢ Ⅎ x (φ \land m \in Z)$
107	73	a1i	$⊢ (φ \land m \in Z) \to dom F (m) \in V$
108	29	ffvelrnda	$⊢ ((φ \land m \in Z) \land x \in dom F (m)) \to F (m) (x) \in ℝ$
109	29	feqmptd	$⊢ (φ \land m \in Z) \to F (m) = (x \in dom F (m) ⟼ F (m) (x))$
110	109 27	eqeltrrd	$⊢ (φ \land m \in Z) \to (x \in dom F (m) ⟼ F (m) (x)) \in SMblFn (S)$
111	106 26 107 108 110	smfneg	$⊢ (φ \land m \in Z) \to (x \in dom F (m) ⟼ - F (m) (x)) \in SMblFn (S)$
112		eqid	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ\} = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ\}$
113		eqid	$⊢ (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ\} ⟼ lim sup ((m \in Z ⟼ - F (m) (x)))) = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ\} ⟼ lim sup ((m \in Z ⟼ - F (m) (x))))$
114	102 70 103 1 2 3 105 111 112 113	smflimsupmpt	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ - F (m) (x))) \in ℝ\} ⟼ lim sup ((m \in Z ⟼ - F (m) (x)))) \in SMblFn (S)$
115	101 114	eqeltrd	$⊢ φ \to (x \in D ⟼ lim sup ((m \in Z ⟼ - F (m) (x)))) \in SMblFn (S)$
116	70 3 82 65 115	smfneg	$⊢ φ \to (x \in D ⟼ - lim sup ((m \in Z ⟼ - F (m) (x)))) \in SMblFn (S)$
117	69 116	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfliminflem

Proof