smflimsuplem2

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflimsuplem2.p	$⊢ Ⅎ m φ$
	smflimsuplem2.m	$⊢ φ \to M \in ℤ$
	smflimsuplem2.z	$⊢ Z = ℤ_{\geq M}$
	smflimsuplem2.s	$⊢ φ \to S \in SAlg$
	smflimsuplem2.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimsuplem2.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
	smflimsuplem2.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
	smflimsuplem2.n	$⊢ φ \to n \in Z$
	smflimsuplem2.r	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (X))) \in ℝ$
	smflimsuplem2.x	$⊢ φ \to X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
Assertion	smflimsuplem2	$⊢ φ \to X \in dom H (n)$

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem2.p	$⊢ Ⅎ m φ$
2		smflimsuplem2.m	$⊢ φ \to M \in ℤ$
3		smflimsuplem2.z	$⊢ Z = ℤ_{\geq M}$
4		smflimsuplem2.s	$⊢ φ \to S \in SAlg$
5		smflimsuplem2.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
6		smflimsuplem2.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
7		smflimsuplem2.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
8		smflimsuplem2.n	$⊢ φ \to n \in Z$
9		smflimsuplem2.r	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (X))) \in ℝ$
10		smflimsuplem2.x	$⊢ φ \to X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
11		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
12	8 3	eleqtrdi	$⊢ φ \to n \in ℤ_{\geq M}$
13		uzss	$⊢ n \in ℤ_{\geq M} \to ℤ_{\geq n} \subseteq ℤ_{\geq M}$
14	12 13	syl	$⊢ φ \to ℤ_{\geq n} \subseteq ℤ_{\geq M}$
15	14 3	sseqtrrdi	$⊢ φ \to ℤ_{\geq n} \subseteq Z$
16	15	adantr	$⊢ (φ \land m \in ℤ_{\geq n}) \to ℤ_{\geq n} \subseteq Z$
17		simpr	$⊢ (φ \land m \in ℤ_{\geq n}) \to m \in ℤ_{\geq n}$
18	16 17	sseldd	$⊢ (φ \land m \in ℤ_{\geq n}) \to m \in Z$
19	4	adantr	$⊢ (φ \land m \in Z) \to S \in SAlg$
20	5	ffvelcdmda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
21		eqid	$⊢ dom F (m) = dom F (m)$
22	19 20 21	smff	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
23	18 22	syldan	$⊢ (φ \land m \in ℤ_{\geq n}) \to F (m) : dom F (m) ⟶ ℝ$
24		iinss2	$⊢ m \in ℤ_{\geq n} \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \subseteq dom F (m)$
25	24	adantl	$⊢ (φ \land m \in ℤ_{\geq n}) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \subseteq dom F (m)$
26	10	adantr	$⊢ (φ \land m \in ℤ_{\geq n}) \to X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
27	25 26	sseldd	$⊢ (φ \land m \in ℤ_{\geq n}) \to X \in dom F (m)$
28	23 27	ffvelcdmd	$⊢ (φ \land m \in ℤ_{\geq n}) \to F (m) (X) \in ℝ$
29		nfmpt1	$⊢ \underline{Ⅎ} m (m \in ℤ_{\geq n} ⟼ F (m) (X))$
30		nfmpt1	$⊢ \underline{Ⅎ} m (m \in ℤ_{\geq M} ⟼ F (m) (X))$
31		eluzelz	$⊢ n \in ℤ_{\geq M} \to n \in ℤ$
32	12 31	syl	$⊢ φ \to n \in ℤ$
33		eqid	$⊢ (m \in ℤ_{\geq n} ⟼ F (m) (X)) = (m \in ℤ_{\geq n} ⟼ F (m) (X))$
34	1 28 33	fmptdf	$⊢ φ \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) : ℤ_{\geq n} ⟶ ℝ$
35	34	ffnd	$⊢ φ \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) Fn ℤ_{\geq n}$
36		nfcv	$⊢ \underline{Ⅎ} m ℤ_{\geq M}$
37		fvexd	$⊢ (φ \land m \in ℤ_{\geq M}) \to F (m) (X) \in V$
38	36 1 37	mptfnd	$⊢ φ \to (m \in ℤ_{\geq M} ⟼ F (m) (X)) Fn ℤ_{\geq M}$
39	33	a1i	$⊢ φ \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) = (m \in ℤ_{\geq n} ⟼ F (m) (X))$
40		fvexd	$⊢ (φ \land m \in ℤ_{\geq n}) \to F (m) (X) \in V$
41	39 40	fvmpt2d	$⊢ (φ \land m \in ℤ_{\geq n}) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) (m) = F (m) (X)$
42	18 3	eleqtrdi	$⊢ (φ \land m \in ℤ_{\geq n}) \to m \in ℤ_{\geq M}$
43		eqid	$⊢ (m \in ℤ_{\geq M} ⟼ F (m) (X)) = (m \in ℤ_{\geq M} ⟼ F (m) (X))$
44	43	fvmpt2	$⊢ (m \in ℤ_{\geq M} \land F (m) (X) \in V) \to (m \in ℤ_{\geq M} ⟼ F (m) (X)) (m) = F (m) (X)$
45	42 40 44	syl2anc	$⊢ (φ \land m \in ℤ_{\geq n}) \to (m \in ℤ_{\geq M} ⟼ F (m) (X)) (m) = F (m) (X)$
46	41 45	eqtr4d	$⊢ (φ \land m \in ℤ_{\geq n}) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) (m) = (m \in ℤ_{\geq M} ⟼ F (m) (X)) (m)$
47	1 29 30 32 35 2 38 32 46	limsupequz	$⊢ φ \to lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (X))) = lim sup ((m \in ℤ_{\geq M} ⟼ F (m) (X)))$
48	3	eqcomi	$⊢ ℤ_{\geq M} = Z$
49	48	mpteq1i	$⊢ (m \in ℤ_{\geq M} ⟼ F (m) (X)) = (m \in Z ⟼ F (m) (X))$
50	49	fveq2i	$⊢ lim sup ((m \in ℤ_{\geq M} ⟼ F (m) (X))) = lim sup ((m \in Z ⟼ F (m) (X)))$
51	50	a1i	$⊢ φ \to lim sup ((m \in ℤ_{\geq M} ⟼ F (m) (X))) = lim sup ((m \in Z ⟼ F (m) (X)))$
52	47 51	eqtrd	$⊢ φ \to lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (X))) = lim sup ((m \in Z ⟼ F (m) (X)))$
53	9	renepnfd	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (X))) \neq +∞$
54	52 53	eqnetrd	$⊢ φ \to lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (X))) \neq +∞$
55	1 11 28 54	limsupubuzmpt	$⊢ φ \to \exists y \in ℝ \forall m \in ℤ_{\geq n} F (m) (X) \leq y$
56		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
57		ne0i	$⊢ n \in ℤ_{\geq n} \to ℤ_{\geq n} \neq \emptyset$
58	32 56 57	3syl	$⊢ φ \to ℤ_{\geq n} \neq \emptyset$
59	1 58 28	supxrre3rnmpt	$⊢ φ \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{*} <) \in ℝ \leftrightarrow \exists y \in ℝ \forall m \in ℤ_{\geq n} F (m) (X) \leq y)$
60	55 59	mpbird	$⊢ φ \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{*} <) \in ℝ$
61	10 60	jca	$⊢ φ \to (X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{*} <) \in ℝ)$
62		fveq2	$⊢ x = y \to F (m) (x) = F (m) (y)$
63	62	mpteq2dv	$⊢ x = y \to (m \in ℤ_{\geq n} ⟼ F (m) (x)) = (m \in ℤ_{\geq n} ⟼ F (m) (y))$
64	63	rneqd	$⊢ x = y \to ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) = ran (m \in ℤ_{\geq n} ⟼ F (m) (y))$
65	64	supeq1d	$⊢ x = y \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <)$
66	65	eleq1d	$⊢ x = y \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ)$
67	66	cbvrabv	$⊢ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{y \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ\}$
68	67	eleq2i	$⊢ X \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} \leftrightarrow X \in \{y \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ\}$
69		fveq2	$⊢ y = X \to F (m) (y) = F (m) (X)$
70	69	mpteq2dv	$⊢ y = X \to (m \in ℤ_{\geq n} ⟼ F (m) (y)) = (m \in ℤ_{\geq n} ⟼ F (m) (X))$
71	70	rneqd	$⊢ y = X \to ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) = ran (m \in ℤ_{\geq n} ⟼ F (m) (X))$
72	71	supeq1d	$⊢ y = X \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{} <)$
73	72	eleq1d	$⊢ y = X \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{} <) \in ℝ)$
74	73	elrab	$⊢ X \in \{y \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ\} \leftrightarrow (X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{} <) \in ℝ)$
75	68 74	bitri	$⊢ X \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} \leftrightarrow (X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (X)) ℝ^{} <) \in ℝ)$
76	61 75	sylibr	$⊢ φ \to X \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
77		id	$⊢ φ \to φ$
78	7	a1i	$⊢ φ \to H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
79		nfcv	$⊢ \underline{Ⅎ} x Z$
80		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
81	79 80	nfmpt	$⊢ \underline{Ⅎ} x (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
82	6 81	nfcxfr	$⊢ \underline{Ⅎ} x E$
83		nfcv	$⊢ \underline{Ⅎ} x n$
84	82 83	nffv	$⊢ \underline{Ⅎ} x E (n)$
85		fvex	$⊢ E (n) \in V$
86	84 85	mptexf	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in V$
87	86	a1i	$⊢ (φ \land n \in Z) \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in V$
88	78 87	fvmpt2d	$⊢ (φ \land n \in Z) \to H (n) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
89	77 8 88	syl2anc	$⊢ φ \to H (n) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
90	89	dmeqd	$⊢ φ \to dom H (n) = dom (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
91		nfcv	$⊢ \underline{Ⅎ} y E (n)$
92		nfcv	$⊢ \underline{Ⅎ} y sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)$
93		nfcv	$⊢ \underline{Ⅎ} x sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{*} <)$
94	84 91 92 93 65	cbvmptf	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) = (y \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <))$
95		xrltso	$⊢ < Or ℝ^{*}$
96	95	supex	$⊢ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{*} <) \in V$
97	96	a1i	$⊢ (φ \land y \in E (n)) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{*} <) \in V$
98	94 97	dmmptd	$⊢ φ \to dom (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) = E (n)$
99		eqid	$⊢ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\}$
100		fvex	$⊢ F (m) \in V$
101	100	dmex	$⊢ dom F (m) \in V$
102	101	rgenw	$⊢ \forall m \in ℤ_{\geq n} dom F (m) \in V$
103	102	a1i	$⊢ φ \to \forall m \in ℤ_{\geq n} dom F (m) \in V$
104	58 103	iinexd	$⊢ φ \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
105	99 104	rabexd	$⊢ φ \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} \in V$
106	6	fvmpt2	$⊢ (n \in Z \land \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} \in V) \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\}$
107	8 105 106	syl2anc	$⊢ φ \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
108	90 98 107	3eqtrrd	$⊢ φ \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} = dom H (n)$
109	76 108	eleqtrd	$⊢ φ \to X \in dom H (n)$

Metamath Proof Explorer

Theorem smflimsuplem2

Proof