smflimsuplem8

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

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem8.m	$⊢ φ \to M \in ℤ$
2		smflimsuplem8.z	$⊢ Z = ℤ_{\geq M}$
3		smflimsuplem8.s	$⊢ φ \to S \in SAlg$
4		smflimsuplem8.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smflimsuplem8.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
6		smflimsuplem8.g	$⊢ G = (x \in D ⟼ lim sup ((m \in Z ⟼ F (m) (x))))$
7		smflimsuplem8.e	$⊢ E = (k \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq k}} dom F (m) \| sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
8		smflimsuplem8.h	$⊢ H = (k \in Z ⟼ (x \in E (k) ⟼ sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{*} <)))$
9	6	a1i	$⊢ φ \to G = (x \in D ⟼ lim sup ((m \in Z ⟼ F (m) (x))))$
10	1 2 3 4 5 7 8	smflimsuplem7	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}$
11		rabidim1	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
12		eliun	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
13	11 12	sylib	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
14	13 5	eleq2s	$⊢ x \in D \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
15	14	adantl	$⊢ (φ \land x \in D) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
16		nfv	$⊢ Ⅎ n (φ \land x \in D)$
17		nfv	$⊢ Ⅎ n lim sup ((m \in Z ⟼ F (m) (x))) = ⇝ ((k \in Z ⟼ H (k) (x)))$
18		nfv	$⊢ Ⅎ k ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m))$
19		nfv	$⊢ Ⅎ m (φ \land x \in D)$
20		nfv	$⊢ Ⅎ m n \in Z$
21		nfcv	$⊢ \underline{Ⅎ} m x$
22		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq n}} dom F (m)$
23	21 22	nfel	$⊢ Ⅎ m x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
24	19 20 23	nf3an	$⊢ Ⅎ m ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m))$
25	1	adantr	$⊢ (φ \land x \in D) \to M \in ℤ$
26	25	3ad2ant1	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to M \in ℤ$
27	3	adantr	$⊢ (φ \land x \in D) \to S \in SAlg$
28	27	3ad2ant1	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to S \in SAlg$
29	4	adantr	$⊢ (φ \land x \in D) \to F : Z ⟶ SMblFn (S)$
30	29	3ad2ant1	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to F : Z ⟶ SMblFn (S)$
31		rabidim2	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
32	31 5	eleq2s	$⊢ x \in D \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
33		fveq2	$⊢ m = y \to F (m) = F (y)$
34	33	fveq1d	$⊢ m = y \to F (m) (x) = F (y) (x)$
35	34	cbvmptv	$⊢ (m \in Z ⟼ F (m) (x)) = (y \in Z ⟼ F (y) (x))$
36		fveq2	$⊢ z = y \to F (z) = F (y)$
37	36	fveq1d	$⊢ z = y \to F (z) (x) = F (y) (x)$
38	37	cbvmptv	$⊢ (z \in Z ⟼ F (z) (x)) = (y \in Z ⟼ F (y) (x))$
39		fveq2	$⊢ z = w \to F (z) = F (w)$
40	39	fveq1d	$⊢ z = w \to F (z) (x) = F (w) (x)$
41	40	cbvmptv	$⊢ (z \in Z ⟼ F (z) (x)) = (w \in Z ⟼ F (w) (x))$
42	35 38 41	3eqtr2i	$⊢ (m \in Z ⟼ F (m) (x)) = (w \in Z ⟼ F (w) (x))$
43	42	fveq2i	$⊢ lim sup ((m \in Z ⟼ F (m) (x))) = lim sup ((w \in Z ⟼ F (w) (x)))$
44	43	eleq1i	$⊢ lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ \leftrightarrow lim sup ((w \in Z ⟼ F (w) (x))) \in ℝ$
45	32 44	sylib	$⊢ x \in D \to lim sup ((w \in Z ⟼ F (w) (x))) \in ℝ$
46	45	adantl	$⊢ (φ \land x \in D) \to lim sup ((w \in Z ⟼ F (w) (x))) \in ℝ$
47	46	3ad2ant1	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to lim sup ((w \in Z ⟼ F (w) (x))) \in ℝ$
48	47 44	sylibr	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
49		simp2	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to n \in Z$
50		simp3	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
51	18 24 26 2 28 30 7 8 48 49 50	smflimsuplem5	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to (k \in ℤ_{\geq n} ⟼ H (k) (x)) ⇝ lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (x)))$
52		fvexd	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ℤ_{\geq n} \in V$
53	2	fvexi	$⊢ Z \in V$
54	53	a1i	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to Z \in V$
55	2 49	eluzelz2d	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to n \in ℤ$
56		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
57	55	uzidd	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to n \in ℤ_{\geq n}$
58	57	uzssd	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ℤ_{\geq n} \subseteq ℤ_{\geq n}$
59	2 49	uzssd2	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ℤ_{\geq n} \subseteq Z$
60		fvexd	$⊢ (((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to H (k) (x) \in V$
61	18 52 54 55 56 58 59 60	climeqmpt	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ((k \in ℤ_{\geq n} ⟼ H (k) (x)) ⇝ lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (x))) \leftrightarrow (k \in Z ⟼ H (k) (x)) ⇝ lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (x))))$
62	51 61	mpbid	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to (k \in Z ⟼ H (k) (x)) ⇝ lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (x)))$
63		simp1l	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to φ$
64		nfv	$⊢ Ⅎ m φ$
65	64 20	nfan	$⊢ Ⅎ m (φ \land n \in Z)$
66	2	eluzelz2	$⊢ n \in Z \to n \in ℤ$
67	66	adantl	$⊢ (φ \land n \in Z) \to n \in ℤ$
68	1	adantr	$⊢ (φ \land n \in Z) \to M \in ℤ$
69		fvexd	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to F (m) (x) \in V$
70		fvexd	$⊢ ((φ \land n \in Z) \land m \in Z) \to F (m) (x) \in V$
71	65 67 68 56 2 69 70	limsupequzmpt	$⊢ (φ \land n \in Z) \to lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (x))) = lim sup ((m \in Z ⟼ F (m) (x)))$
72	63 49 71	syl2anc	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to lim sup ((m \in ℤ_{\geq n} ⟼ F (m) (x))) = lim sup ((m \in Z ⟼ F (m) (x)))$
73	62 72	breqtrd	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to (k \in Z ⟼ H (k) (x)) ⇝ lim sup ((m \in Z ⟼ F (m) (x)))$
74	73	climfvd	$⊢ ((φ \land x \in D) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to lim sup ((m \in Z ⟼ F (m) (x))) = ⇝ ((k \in Z ⟼ H (k) (x)))$
75	74	3exp	$⊢ (φ \land x \in D) \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to lim sup ((m \in Z ⟼ F (m) (x))) = ⇝ ((k \in Z ⟼ H (k) (x)))))$
76	16 17 75	rexlimd	$⊢ (φ \land x \in D) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to lim sup ((m \in Z ⟼ F (m) (x))) = ⇝ ((k \in Z ⟼ H (k) (x))))$
77	15 76	mpd	$⊢ (φ \land x \in D) \to lim sup ((m \in Z ⟼ F (m) (x))) = ⇝ ((k \in Z ⟼ H (k) (x)))$
78	10 77	mpteq12dva	$⊢ φ \to (x \in D ⟼ lim sup ((m \in Z ⟼ F (m) (x)))) = (x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} ⟼ ⇝ ((k \in Z ⟼ H (k) (x))))$
79	9 78	eqtrd	$⊢ φ \to G = (x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} ⟼ ⇝ ((k \in Z ⟼ H (k) (x))))$
80	1 2 3 4 7 8	smflimsuplem3	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} ⟼ ⇝ ((k \in Z ⟼ H (k) (x)))) \in SMblFn (S)$
81	79 80	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smflimsuplem8

Proof