smflimsup

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

Proof

Step	Hyp	Ref	Expression
1		smflimsup.n	$⊢ \underline{Ⅎ} m F$
2		smflimsup.x	$⊢ \underline{Ⅎ} x F$
3		smflimsup.m	$⊢ φ \to M \in ℤ$
4		smflimsup.z	$⊢ Z = ℤ_{\geq M}$
5		smflimsup.s	$⊢ φ \to S \in SAlg$
6		smflimsup.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
7		smflimsup.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
8		smflimsup.g	$⊢ G = (x \in D ⟼ lim sup ((m \in Z ⟼ F (m) (x))))$
9		fveq2	$⊢ n = j \to ℤ_{\geq n} = ℤ_{\geq j}$
10	9	iineq1d	$⊢ n = j \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{m \in ℤ_{\geq j}} dom F (m)$
11		nfcv	$⊢ \underline{Ⅎ} q dom F (m)$
12		nfcv	$⊢ \underline{Ⅎ} m q$
13	1 12	nffv	$⊢ \underline{Ⅎ} m F (q)$
14	13	nfdm	$⊢ \underline{Ⅎ} m dom F (q)$
15		fveq2	$⊢ m = q \to F (m) = F (q)$
16	15	dmeqd	$⊢ m = q \to dom F (m) = dom F (q)$
17	11 14 16	cbviin	$⊢ ⋂_{m \in ℤ_{\geq j}} dom F (m) = ⋂_{q \in ℤ_{\geq j}} dom F (q)$
18	17	a1i	$⊢ n = j \to ⋂_{m \in ℤ_{\geq j}} dom F (m) = ⋂_{q \in ℤ_{\geq j}} dom F (q)$
19	10 18	eqtrd	$⊢ n = j \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{q \in ℤ_{\geq j}} dom F (q)$
20	19	cbviunv	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q)$
21	20	eleq2i	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow x \in ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q)$
22		nfcv	$⊢ \underline{Ⅎ} q F (m) (x)$
23		nfcv	$⊢ \underline{Ⅎ} m x$
24	13 23	nffv	$⊢ \underline{Ⅎ} m F (q) (x)$
25	15	fveq1d	$⊢ m = q \to F (m) (x) = F (q) (x)$
26	22 24 25	cbvmpt	$⊢ (m \in Z ⟼ F (m) (x)) = (q \in Z ⟼ F (q) (x))$
27	26	fveq2i	$⊢ lim sup ((m \in Z ⟼ F (m) (x))) = lim sup ((q \in Z ⟼ F (q) (x)))$
28	27	eleq1i	$⊢ lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ \leftrightarrow lim sup ((q \in Z ⟼ F (q) (x))) \in ℝ$
29	21 28	anbi12i	$⊢ (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \leftrightarrow (x \in ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q) \land lim sup ((q \in Z ⟼ F (q) (x))) \in ℝ)$
30	29	rabbia2	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} = \{x \in ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q) \| lim sup ((q \in Z ⟼ F (q) (x))) \in ℝ\}$
31		nfcv	$⊢ \underline{Ⅎ} x Z$
32		nfcv	$⊢ \underline{Ⅎ} x ℤ_{\geq j}$
33		nfcv	$⊢ \underline{Ⅎ} x q$
34	2 33	nffv	$⊢ \underline{Ⅎ} x F (q)$
35	34	nfdm	$⊢ \underline{Ⅎ} x dom F (q)$
36	32 35	nfiin	$⊢ \underline{Ⅎ} x ⋂_{q \in ℤ_{\geq j}} dom F (q)$
37	31 36	nfiun	$⊢ \underline{Ⅎ} x ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q)$
38		nfcv	$⊢ \underline{Ⅎ} w ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q)$
39		nfv	$⊢ Ⅎ w lim sup ((q \in Z ⟼ F (q) (x))) \in ℝ$
40		nfcv	$⊢ \underline{Ⅎ} x lim sup$
41		nfcv	$⊢ \underline{Ⅎ} x w$
42	34 41	nffv	$⊢ \underline{Ⅎ} x F (q) (w)$
43	31 42	nfmpt	$⊢ \underline{Ⅎ} x (q \in Z ⟼ F (q) (w))$
44	40 43	nffv	$⊢ \underline{Ⅎ} x lim sup ((q \in Z ⟼ F (q) (w)))$
45		nfcv	$⊢ \underline{Ⅎ} x ℝ$
46	44 45	nfel	$⊢ Ⅎ x lim sup ((q \in Z ⟼ F (q) (w))) \in ℝ$
47		fveq2	$⊢ x = w \to F (q) (x) = F (q) (w)$
48	47	mpteq2dv	$⊢ x = w \to (q \in Z ⟼ F (q) (x)) = (q \in Z ⟼ F (q) (w))$
49	48	fveq2d	$⊢ x = w \to lim sup ((q \in Z ⟼ F (q) (x))) = lim sup ((q \in Z ⟼ F (q) (w)))$
50	49	eleq1d	$⊢ x = w \to (lim sup ((q \in Z ⟼ F (q) (x))) \in ℝ \leftrightarrow lim sup ((q \in Z ⟼ F (q) (w))) \in ℝ)$
51	37 38 39 46 50	cbvrabw	$⊢ \{x \in ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q) \| lim sup ((q \in Z ⟼ F (q) (x))) \in ℝ\} = \{w \in ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q) \| lim sup ((q \in Z ⟼ F (q) (w))) \in ℝ\}$
52	7 30 51	3eqtri	$⊢ D = \{w \in ⋃_{j \in Z} ⋂_{q \in ℤ_{\geq j}} dom F (q) \| lim sup ((q \in Z ⟼ F (q) (w))) \in ℝ\}$
53	27	mpteq2i	$⊢ (x \in D ⟼ lim sup ((m \in Z ⟼ F (m) (x)))) = (x \in D ⟼ lim sup ((q \in Z ⟼ F (q) (x))))$
54		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
55	7 54	nfcxfr	$⊢ \underline{Ⅎ} x D$
56		nfcv	$⊢ \underline{Ⅎ} w D$
57		nfcv	$⊢ \underline{Ⅎ} w lim sup ((q \in Z ⟼ F (q) (x)))$
58	55 56 57 44 49	cbvmptf	$⊢ (x \in D ⟼ lim sup ((q \in Z ⟼ F (q) (x)))) = (w \in D ⟼ lim sup ((q \in Z ⟼ F (q) (w))))$
59	8 53 58	3eqtri	$⊢ G = (w \in D ⟼ lim sup ((q \in Z ⟼ F (q) (w))))$
60		nfcv	$⊢ \underline{Ⅎ} x ℤ_{\geq i}$
61	60 35	nfiin	$⊢ \underline{Ⅎ} x ⋂_{q \in ℤ_{\geq i}} dom F (q)$
62		nfcv	$⊢ \underline{Ⅎ} w ⋂_{q \in ℤ_{\geq i}} dom F (q)$
63		nfv	$⊢ Ⅎ w sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{*} <) \in ℝ$
64	60 42	nfmpt	$⊢ \underline{Ⅎ} x (q \in ℤ_{\geq i} ⟼ F (q) (w))$
65	64	nfrn	$⊢ \underline{Ⅎ} x ran (q \in ℤ_{\geq i} ⟼ F (q) (w))$
66		nfcv	$⊢ \underline{Ⅎ} x ℝ^{*}$
67		nfcv	$⊢ \underline{Ⅎ} x <$
68	65 66 67	nfsup	$⊢ \underline{Ⅎ} x sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{*} <)$
69	68 45	nfel	$⊢ Ⅎ x sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{*} <) \in ℝ$
70	47	mpteq2dv	$⊢ x = w \to (q \in ℤ_{\geq i} ⟼ F (q) (x)) = (q \in ℤ_{\geq i} ⟼ F (q) (w))$
71	70	rneqd	$⊢ x = w \to ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) = ran (q \in ℤ_{\geq i} ⟼ F (q) (w))$
72	71	supeq1d	$⊢ x = w \to sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) = sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{} <)$
73	72	eleq1d	$⊢ x = w \to (sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{} <) \in ℝ)$
74	61 62 63 69 73	cbvrabw	$⊢ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\} = \{w \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{} <) \in ℝ\}$
75	74	a1i	$⊢ i = k \to \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\} = \{w \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{} <) \in ℝ\}$
76		fveq2	$⊢ i = k \to ℤ_{\geq i} = ℤ_{\geq k}$
77	76	iineq1d	$⊢ i = k \to ⋂_{q \in ℤ_{\geq i}} dom F (q) = ⋂_{q \in ℤ_{\geq k}} dom F (q)$
78	77	eleq2d	$⊢ i = k \to (w \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \leftrightarrow w \in ⋂_{q \in ℤ_{\geq k}} dom F (q))$
79	76	mpteq1d	$⊢ i = k \to (q \in ℤ_{\geq i} ⟼ F (q) (w)) = (q \in ℤ_{\geq k} ⟼ F (q) (w))$
80	79	rneqd	$⊢ i = k \to ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) = ran (q \in ℤ_{\geq k} ⟼ F (q) (w))$
81	80	supeq1d	$⊢ i = k \to sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{} <) = sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <)$
82	81	eleq1d	$⊢ i = k \to (sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <) \in ℝ)$
83	78 82	anbi12d	$⊢ i = k \to ((w \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \land sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{} <) \in ℝ) \leftrightarrow (w \in ⋂_{q \in ℤ_{\geq k}} dom F (q) \land sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <) \in ℝ))$
84	83	rabbidva2	$⊢ i = k \to \{w \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (w)) ℝ^{} <) \in ℝ\} = \{w \in ⋂_{q \in ℤ_{\geq k}} dom F (q) \| sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <) \in ℝ\}$
85	75 84	eqtrd	$⊢ i = k \to \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\} = \{w \in ⋂_{q \in ℤ_{\geq k}} dom F (q) \| sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <) \in ℝ\}$
86	85	cbvmptv	$⊢ (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) = (k \in Z ⟼ \{w \in ⋂_{q \in ℤ_{\geq k}} dom F (q) \| sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <) \in ℝ\})$
87		fveq2	$⊢ y = w \to F (p) (y) = F (p) (w)$
88	87	mpteq2dv	$⊢ y = w \to (p \in ℤ_{\geq l} ⟼ F (p) (y)) = (p \in ℤ_{\geq l} ⟼ F (p) (w))$
89	88	rneqd	$⊢ y = w \to ran (p \in ℤ_{\geq l} ⟼ F (p) (y)) = ran (p \in ℤ_{\geq l} ⟼ F (p) (w))$
90	89	supeq1d	$⊢ y = w \to sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (y)) ℝ^{} <) = sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (w)) ℝ^{} <)$
91	90	cbvmptv	$⊢ (y \in (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (y)) ℝ^{} <)) = (w \in (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (w)) ℝ^{} <))$
92		fveq2	$⊢ p = q \to F (p) = F (q)$
93	92	dmeqd	$⊢ p = q \to dom F (p) = dom F (q)$
94	93	cbviinv	$⊢ ⋂_{p \in ℤ_{\geq i}} dom F (p) = ⋂_{q \in ℤ_{\geq i}} dom F (q)$
95	94	eleq2i	$⊢ x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \leftrightarrow x \in ⋂_{q \in ℤ_{\geq i}} dom F (q)$
96		nfcv	$⊢ \underline{Ⅎ} q F (p) (x)$
97		nfcv	$⊢ \underline{Ⅎ} p F (q)$
98		nfcv	$⊢ \underline{Ⅎ} p x$
99	97 98	nffv	$⊢ \underline{Ⅎ} p F (q) (x)$
100	92	fveq1d	$⊢ p = q \to F (p) (x) = F (q) (x)$
101	96 99 100	cbvmpt	$⊢ (p \in ℤ_{\geq i} ⟼ F (p) (x)) = (q \in ℤ_{\geq i} ⟼ F (q) (x))$
102	101	rneqi	$⊢ ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) = ran (q \in ℤ_{\geq i} ⟼ F (q) (x))$
103	102	supeq1i	$⊢ sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) = sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <)$
104	103	eleq1i	$⊢ sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ$
105	95 104	anbi12i	$⊢ (x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \land sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ) \leftrightarrow (x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \land sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ)$
106	105	rabbia2	$⊢ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}$
107	106	mpteq2i	$⊢ (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) = (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\})$
108	107	fveq1i	$⊢ (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) (l) = (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (l)$
109	92	fveq1d	$⊢ p = q \to F (p) (w) = F (q) (w)$
110	109	cbvmptv	$⊢ (p \in ℤ_{\geq l} ⟼ F (p) (w)) = (q \in ℤ_{\geq l} ⟼ F (q) (w))$
111	110	rneqi	$⊢ ran (p \in ℤ_{\geq l} ⟼ F (p) (w)) = ran (q \in ℤ_{\geq l} ⟼ F (q) (w))$
112	111	supeq1i	$⊢ sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (w)) ℝ^{} <) = sup (ran (q \in ℤ_{\geq l} ⟼ F (q) (w)) ℝ^{} <)$
113	108 112	mpteq12i	$⊢ (w \in (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (w)) ℝ^{} <)) = (w \in (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (q \in ℤ_{\geq l} ⟼ F (q) (w)) ℝ^{} <))$
114	91 113	eqtri	$⊢ (y \in (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (y)) ℝ^{} <)) = (w \in (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (q \in ℤ_{\geq l} ⟼ F (q) (w)) ℝ^{} <))$
115	114	a1i	$⊢ l = k \to (y \in (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (y)) ℝ^{} <)) = (w \in (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (q \in ℤ_{\geq l} ⟼ F (q) (w)) ℝ^{} <))$
116		fveq2	$⊢ l = k \to (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (l) = (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (k)$
117		fveq2	$⊢ l = k \to ℤ_{\geq l} = ℤ_{\geq k}$
118	117	mpteq1d	$⊢ l = k \to (q \in ℤ_{\geq l} ⟼ F (q) (w)) = (q \in ℤ_{\geq k} ⟼ F (q) (w))$
119	118	rneqd	$⊢ l = k \to ran (q \in ℤ_{\geq l} ⟼ F (q) (w)) = ran (q \in ℤ_{\geq k} ⟼ F (q) (w))$
120	119	supeq1d	$⊢ l = k \to sup (ran (q \in ℤ_{\geq l} ⟼ F (q) (w)) ℝ^{} <) = sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <)$
121	116 120	mpteq12dv	$⊢ l = k \to (w \in (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (q \in ℤ_{\geq l} ⟼ F (q) (w)) ℝ^{} <)) = (w \in (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (k) ⟼ sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <))$
122	115 121	eqtrd	$⊢ l = k \to (y \in (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (y)) ℝ^{} <)) = (w \in (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (k) ⟼ sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <))$
123	122	cbvmptv	$⊢ (l \in Z ⟼ (y \in (i \in Z ⟼ \{x \in ⋂_{p \in ℤ_{\geq i}} dom F (p) \| sup (ran (p \in ℤ_{\geq i} ⟼ F (p) (x)) ℝ^{} <) \in ℝ\}) (l) ⟼ sup (ran (p \in ℤ_{\geq l} ⟼ F (p) (y)) ℝ^{} <))) = (k \in Z ⟼ (w \in (i \in Z ⟼ \{x \in ⋂_{q \in ℤ_{\geq i}} dom F (q) \| sup (ran (q \in ℤ_{\geq i} ⟼ F (q) (x)) ℝ^{} <) \in ℝ\}) (k) ⟼ sup (ran (q \in ℤ_{\geq k} ⟼ F (q) (w)) ℝ^{} <)))$
124	3 4 5 6 52 59 86 123	smflimsuplem8	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smflimsup

Proof