smflimsuplem6

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	smflimsuplem6.a	$⊢ Ⅎ n φ$
	smflimsuplem6.b	$⊢ Ⅎ m φ$
	smflimsuplem6.m	$⊢ φ \to M \in ℤ$
	smflimsuplem6.z	$⊢ Z = ℤ_{\geq M}$
	smflimsuplem6.s	$⊢ φ \to S \in SAlg$
	smflimsuplem6.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimsuplem6.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
	smflimsuplem6.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
	smflimsuplem6.r	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (X))) \in ℝ$
	smflimsuplem6.n	$⊢ φ \to N \in Z$
	smflimsuplem6.x	$⊢ φ \to X \in ⋂_{m \in ℤ_{\geq N}} dom F (m)$
Assertion	smflimsuplem6	$⊢ φ \to (n \in Z ⟼ H (n) (X)) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem6.a	$⊢ Ⅎ n φ$
2		smflimsuplem6.b	$⊢ Ⅎ m φ$
3		smflimsuplem6.m	$⊢ φ \to M \in ℤ$
4		smflimsuplem6.z	$⊢ Z = ℤ_{\geq M}$
5		smflimsuplem6.s	$⊢ φ \to S \in SAlg$
6		smflimsuplem6.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
7		smflimsuplem6.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
8		smflimsuplem6.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
9		smflimsuplem6.r	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (X))) \in ℝ$
10		smflimsuplem6.n	$⊢ φ \to N \in Z$
11		smflimsuplem6.x	$⊢ φ \to X \in ⋂_{m \in ℤ_{\geq N}} dom F (m)$
12	4	fvexi	$⊢ Z \in V$
13	12	a1i	$⊢ φ \to Z \in V$
14	13	mptexd	$⊢ φ \to (n \in Z ⟼ H (n) (X)) \in V$
15		fvexd	$⊢ φ \to lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X))) \in V$
16	1 2 3 4 5 6 7 8 9 10 11	smflimsuplem5	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ H (n) (X)) ⇝ lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X)))$
17		fvexd	$⊢ φ \to ℤ_{\geq N} \in V$
18	4	eluzelz2	$⊢ N \in Z \to N \in ℤ$
19	10 18	syl	$⊢ φ \to N \in ℤ$
20		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
21	4	eleq2i	$⊢ N \in Z \leftrightarrow N \in ℤ_{\geq M}$
22	21	biimpi	$⊢ N \in Z \to N \in ℤ_{\geq M}$
23		uzss	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
24	22 23	syl	$⊢ N \in Z \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
25	24 4	sseqtrrdi	$⊢ N \in Z \to ℤ_{\geq N} \subseteq Z$
26	10 25	syl	$⊢ φ \to ℤ_{\geq N} \subseteq Z$
27		ssid	$⊢ ℤ_{\geq N} \subseteq ℤ_{\geq N}$
28	27	a1i	$⊢ φ \to ℤ_{\geq N} \subseteq ℤ_{\geq N}$
29		fvexd	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) (X) \in V$
30	1 13 17 19 20 26 28 29	climeqmpt	$⊢ φ \to ((n \in Z ⟼ H (n) (X)) ⇝ lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X))) \leftrightarrow (n \in ℤ_{\geq N} ⟼ H (n) (X)) ⇝ lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X))))$
31	16 30	mpbird	$⊢ φ \to (n \in Z ⟼ H (n) (X)) ⇝ lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X)))$
32		breldmg	$⊢ ((n \in Z ⟼ H (n) (X)) \in V \land lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X))) \in V \land (n \in Z ⟼ H (n) (X)) ⇝ lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (X)))) \to (n \in Z ⟼ H (n) (X)) \in dom ⇝$
33	14 15 31 32	syl3anc	$⊢ φ \to (n \in Z ⟼ H (n) (X)) \in dom ⇝$

Metamath Proof Explorer

Theorem smflimsuplem6

Proof