mbflimsup

Description: The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	mbflimsup.1	$⊢ Z = ℤ_{\geq M}$
	mbflimsup.2	$⊢ G = (x \in A ⟼ lim sup ((n \in Z ⟼ B)))$
	mbflimsup.h	$⊢ H = (m \in ℝ ⟼ sup ((n \in Z ⟼ B) [[m, +∞)] \cap ℝ^{} ℝ^{} <))$
	mbflimsup.3	$⊢ φ \to M \in ℤ$
	mbflimsup.4	$⊢ (φ \land x \in A) \to lim sup ((n \in Z ⟼ B)) \in ℝ$
	mbflimsup.5	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in MblFn$
	mbflimsup.6	$⊢ (φ \land (n \in Z \land x \in A)) \to B \in ℝ$
Assertion	mbflimsup	$⊢ φ \to G \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbflimsup.1	$⊢ Z = ℤ_{\geq M}$
2		mbflimsup.2	$⊢ G = (x \in A ⟼ lim sup ((n \in Z ⟼ B)))$
3		mbflimsup.h	$⊢ H = (m \in ℝ ⟼ sup ((n \in Z ⟼ B) [[m, +∞)] \cap ℝ^{} ℝ^{} <))$
4		mbflimsup.3	$⊢ φ \to M \in ℤ$
5		mbflimsup.4	$⊢ (φ \land x \in A) \to lim sup ((n \in Z ⟼ B)) \in ℝ$
6		mbflimsup.5	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in MblFn$
7		mbflimsup.6	$⊢ (φ \land (n \in Z \land x \in A)) \to B \in ℝ$
8	1	fvexi	$⊢ Z \in V$
9	8	mptex	$⊢ (n \in Z ⟼ B) \in V$
10	9	a1i	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) \in V$
11		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
12	1 11	eqsstri	$⊢ Z \subseteq ℤ$
13		zssre	$⊢ ℤ \subseteq ℝ$
14	12 13	sstri	$⊢ Z \subseteq ℝ$
15	14	a1i	$⊢ (φ \land x \in A) \to Z \subseteq ℝ$
16	1	uzsup	$⊢ M \in ℤ \to sup (Z ℝ^{*} <) = +∞$
17	4 16	syl	$⊢ φ \to sup (Z ℝ^{*} <) = +∞$
18	17	adantr	$⊢ (φ \land x \in A) \to sup (Z ℝ^{*} <) = +∞$
19	3 10 15 18	limsupval2	$⊢ (φ \land x \in A) \to lim sup ((n \in Z ⟼ B)) = sup (H [Z] ℝ^{*} <)$
20		imassrn	$⊢ H [Z] \subseteq ran H$
21	4	adantr	$⊢ (φ \land x \in A) \to M \in ℤ$
22	7	anass1rs	$⊢ ((φ \land x \in A) \land n \in Z) \to B \in ℝ$
23	22	fmpttd	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) : Z ⟶ ℝ$
24	5	ltpnfd	$⊢ (φ \land x \in A) \to lim sup ((n \in Z ⟼ B)) < +∞$
25	3 1	limsupgre	$⊢ (M \in ℤ \land (n \in Z ⟼ B) : Z ⟶ ℝ \land lim sup ((n \in Z ⟼ B)) < +∞) \to H : ℝ ⟶ ℝ$
26	21 23 24 25	syl3anc	$⊢ (φ \land x \in A) \to H : ℝ ⟶ ℝ$
27	26	frnd	$⊢ (φ \land x \in A) \to ran H \subseteq ℝ$
28	20 27	sstrid	$⊢ (φ \land x \in A) \to H [Z] \subseteq ℝ$
29	26	fdmd	$⊢ (φ \land x \in A) \to dom H = ℝ$
30	29	ineq1d	$⊢ (φ \land x \in A) \to dom H \cap Z = ℝ \cap Z$
31		sseqin2	$⊢ Z \subseteq ℝ \leftrightarrow ℝ \cap Z = Z$
32	14 31	mpbi	$⊢ ℝ \cap Z = Z$
33	30 32	eqtrdi	$⊢ (φ \land x \in A) \to dom H \cap Z = Z$
34		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
35	4 34	syl	$⊢ φ \to M \in ℤ_{\geq M}$
36	35 1	eleqtrrdi	$⊢ φ \to M \in Z$
37	36	adantr	$⊢ (φ \land x \in A) \to M \in Z$
38	37	ne0d	$⊢ (φ \land x \in A) \to Z \neq \emptyset$
39	33 38	eqnetrd	$⊢ (φ \land x \in A) \to dom H \cap Z \neq \emptyset$
40		imadisj	$⊢ H [Z] = \emptyset \leftrightarrow dom H \cap Z = \emptyset$
41	40	necon3bii	$⊢ H [Z] \neq \emptyset \leftrightarrow dom H \cap Z \neq \emptyset$
42	39 41	sylibr	$⊢ (φ \land x \in A) \to H [Z] \neq \emptyset$
43	5	leidd	$⊢ (φ \land x \in A) \to lim sup ((n \in Z ⟼ B)) \leq lim sup ((n \in Z ⟼ B))$
44	22	rexrd	$⊢ ((φ \land x \in A) \land n \in Z) \to B \in ℝ^{*}$
45	44	fmpttd	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) : Z ⟶ ℝ^{*}$
46	5	rexrd	$⊢ (φ \land x \in A) \to lim sup ((n \in Z ⟼ B)) \in ℝ^{*}$
47	3	limsuple	$⊢ (Z \subseteq ℝ \land (n \in Z ⟼ B) : Z ⟶ ℝ^{} \land lim sup ((n \in Z ⟼ B)) \in ℝ^{}) \to (lim sup ((n \in Z ⟼ B)) \leq lim sup ((n \in Z ⟼ B)) \leftrightarrow \forall y \in ℝ lim sup ((n \in Z ⟼ B)) \leq H (y))$
48	15 45 46 47	syl3anc	$⊢ (φ \land x \in A) \to (lim sup ((n \in Z ⟼ B)) \leq lim sup ((n \in Z ⟼ B)) \leftrightarrow \forall y \in ℝ lim sup ((n \in Z ⟼ B)) \leq H (y))$
49	43 48	mpbid	$⊢ (φ \land x \in A) \to \forall y \in ℝ lim sup ((n \in Z ⟼ B)) \leq H (y)$
50		ssralv	$⊢ Z \subseteq ℝ \to (\forall y \in ℝ lim sup ((n \in Z ⟼ B)) \leq H (y) \to \forall y \in Z lim sup ((n \in Z ⟼ B)) \leq H (y))$
51	14 49 50	mpsyl	$⊢ (φ \land x \in A) \to \forall y \in Z lim sup ((n \in Z ⟼ B)) \leq H (y)$
52	3	limsupgf	$⊢ H : ℝ ⟶ ℝ^{*}$
53		ffn	$⊢ H : ℝ ⟶ ℝ^{*} \to H Fn ℝ$
54	52 53	ax-mp	$⊢ H Fn ℝ$
55		breq2	$⊢ z = H (y) \to (lim sup ((n \in Z ⟼ B)) \leq z \leftrightarrow lim sup ((n \in Z ⟼ B)) \leq H (y))$
56	55	ralima	$⊢ (H Fn ℝ \land Z \subseteq ℝ) \to (\forall z \in H [Z] lim sup ((n \in Z ⟼ B)) \leq z \leftrightarrow \forall y \in Z lim sup ((n \in Z ⟼ B)) \leq H (y))$
57	54 15 56	sylancr	$⊢ (φ \land x \in A) \to (\forall z \in H [Z] lim sup ((n \in Z ⟼ B)) \leq z \leftrightarrow \forall y \in Z lim sup ((n \in Z ⟼ B)) \leq H (y))$
58	51 57	mpbird	$⊢ (φ \land x \in A) \to \forall z \in H [Z] lim sup ((n \in Z ⟼ B)) \leq z$
59		breq1	$⊢ y = lim sup ((n \in Z ⟼ B)) \to (y \leq z \leftrightarrow lim sup ((n \in Z ⟼ B)) \leq z)$
60	59	ralbidv	$⊢ y = lim sup ((n \in Z ⟼ B)) \to (\forall z \in H [Z] y \leq z \leftrightarrow \forall z \in H [Z] lim sup ((n \in Z ⟼ B)) \leq z)$
61	60	rspcev	$⊢ (lim sup ((n \in Z ⟼ B)) \in ℝ \land \forall z \in H [Z] lim sup ((n \in Z ⟼ B)) \leq z) \to \exists y \in ℝ \forall z \in H [Z] y \leq z$
62	5 58 61	syl2anc	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall z \in H [Z] y \leq z$
63		infxrre	$⊢ (H [Z] \subseteq ℝ \land H [Z] \neq \emptyset \land \exists y \in ℝ \forall z \in H [Z] y \leq z) \to sup (H [Z] ℝ^{*} <) = sup (H [Z] ℝ <)$
64	28 42 62 63	syl3anc	$⊢ (φ \land x \in A) \to sup (H [Z] ℝ^{*} <) = sup (H [Z] ℝ <)$
65		df-ima	$⊢ H [Z] = ran ({H ↾}_{Z})$
66	26	feqmptd	$⊢ (φ \land x \in A) \to H = (i \in ℝ ⟼ H (i))$
67	66	reseq1d	$⊢ (φ \land x \in A) \to {H ↾}_{Z} = {(i \in ℝ ⟼ H (i)) ↾}_{Z}$
68		resmpt	$⊢ Z \subseteq ℝ \to {(i \in ℝ ⟼ H (i)) ↾}_{Z} = (i \in Z ⟼ H (i))$
69	14 68	ax-mp	$⊢ {(i \in ℝ ⟼ H (i)) ↾}_{Z} = (i \in Z ⟼ H (i))$
70	67 69	eqtrdi	$⊢ (φ \land x \in A) \to {H ↾}_{Z} = (i \in Z ⟼ H (i))$
71	14	sseli	$⊢ i \in Z \to i \in ℝ$
72		ffvelrn	$⊢ (H : ℝ ⟶ ℝ \land i \in ℝ) \to H (i) \in ℝ$
73	26 71 72	syl2an	$⊢ ((φ \land x \in A) \land i \in Z) \to H (i) \in ℝ$
74	73	rexrd	$⊢ ((φ \land x \in A) \land i \in Z) \to H (i) \in ℝ^{*}$
75		simplll	$⊢ (((φ \land x \in A) \land i \in Z) \land n \in ℤ_{\geq i}) \to φ$
76	1	uztrn2	$⊢ (i \in Z \land n \in ℤ_{\geq i}) \to n \in Z$
77	76	adantll	$⊢ (((φ \land x \in A) \land i \in Z) \land n \in ℤ_{\geq i}) \to n \in Z$
78		simpllr	$⊢ (((φ \land x \in A) \land i \in Z) \land n \in ℤ_{\geq i}) \to x \in A$
79	75 77 78 7	syl12anc	$⊢ (((φ \land x \in A) \land i \in Z) \land n \in ℤ_{\geq i}) \to B \in ℝ$
80	79	fmpttd	$⊢ ((φ \land x \in A) \land i \in Z) \to (n \in ℤ_{\geq i} ⟼ B) : ℤ_{\geq i} ⟶ ℝ$
81	80	frnd	$⊢ ((φ \land x \in A) \land i \in Z) \to ran (n \in ℤ_{\geq i} ⟼ B) \subseteq ℝ$
82		eqid	$⊢ (n \in ℤ_{\geq i} ⟼ B) = (n \in ℤ_{\geq i} ⟼ B)$
83	82 79	dmmptd	$⊢ ((φ \land x \in A) \land i \in Z) \to dom (n \in ℤ_{\geq i} ⟼ B) = ℤ_{\geq i}$
84		simpr	$⊢ (φ \land i \in Z) \to i \in Z$
85	84 1	eleqtrdi	$⊢ (φ \land i \in Z) \to i \in ℤ_{\geq M}$
86		eluzelz	$⊢ i \in ℤ_{\geq M} \to i \in ℤ$
87	85 86	syl	$⊢ (φ \land i \in Z) \to i \in ℤ$
88	87	adantlr	$⊢ ((φ \land x \in A) \land i \in Z) \to i \in ℤ$
89		uzid	$⊢ i \in ℤ \to i \in ℤ_{\geq i}$
90		ne0i	$⊢ i \in ℤ_{\geq i} \to ℤ_{\geq i} \neq \emptyset$
91	88 89 90	3syl	$⊢ ((φ \land x \in A) \land i \in Z) \to ℤ_{\geq i} \neq \emptyset$
92	83 91	eqnetrd	$⊢ ((φ \land x \in A) \land i \in Z) \to dom (n \in ℤ_{\geq i} ⟼ B) \neq \emptyset$
93		dm0rn0	$⊢ dom (n \in ℤ_{\geq i} ⟼ B) = \emptyset \leftrightarrow ran (n \in ℤ_{\geq i} ⟼ B) = \emptyset$
94	93	necon3bii	$⊢ dom (n \in ℤ_{\geq i} ⟼ B) \neq \emptyset \leftrightarrow ran (n \in ℤ_{\geq i} ⟼ B) \neq \emptyset$
95	92 94	sylib	$⊢ ((φ \land x \in A) \land i \in Z) \to ran (n \in ℤ_{\geq i} ⟼ B) \neq \emptyset$
96	85	adantlr	$⊢ ((φ \land x \in A) \land i \in Z) \to i \in ℤ_{\geq M}$
97		uzss	$⊢ i \in ℤ_{\geq M} \to ℤ_{\geq i} \subseteq ℤ_{\geq M}$
98	96 97	syl	$⊢ ((φ \land x \in A) \land i \in Z) \to ℤ_{\geq i} \subseteq ℤ_{\geq M}$
99	98 1	sseqtrrdi	$⊢ ((φ \land x \in A) \land i \in Z) \to ℤ_{\geq i} \subseteq Z$
100	73	leidd	$⊢ ((φ \land x \in A) \land i \in Z) \to H (i) \leq H (i)$
101	14	a1i	$⊢ ((φ \land x \in A) \land i \in Z) \to Z \subseteq ℝ$
102	45	adantr	$⊢ ((φ \land x \in A) \land i \in Z) \to (n \in Z ⟼ B) : Z ⟶ ℝ^{*}$
103		simpr	$⊢ ((φ \land x \in A) \land i \in Z) \to i \in Z$
104	14 103	sselid	$⊢ ((φ \land x \in A) \land i \in Z) \to i \in ℝ$
105	3	limsupgle	$⊢ ((Z \subseteq ℝ \land (n \in Z ⟼ B) : Z ⟶ ℝ^{}) \land i \in ℝ \land H (i) \in ℝ^{}) \to (H (i) \leq H (i) \leftrightarrow \forall k \in Z (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i)))$
106	101 102 104 74 105	syl211anc	$⊢ ((φ \land x \in A) \land i \in Z) \to (H (i) \leq H (i) \leftrightarrow \forall k \in Z (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i)))$
107	100 106	mpbid	$⊢ ((φ \land x \in A) \land i \in Z) \to \forall k \in Z (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i))$
108		ssralv	$⊢ ℤ_{\geq i} \subseteq Z \to (\forall k \in Z (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i)) \to \forall k \in ℤ_{\geq i} (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i)))$
109	99 107 108	sylc	$⊢ ((φ \land x \in A) \land i \in Z) \to \forall k \in ℤ_{\geq i} (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i))$
110	99	adantr	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to ℤ_{\geq i} \subseteq Z$
111	110	resmptd	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to {(n \in Z ⟼ B) ↾}_{ℤ_{\geq i}} = (n \in ℤ_{\geq i} ⟼ B)$
112	111	fveq1d	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to ({(n \in Z ⟼ B) ↾}_{ℤ_{\geq i}}) (k) = (n \in ℤ_{\geq i} ⟼ B) (k)$
113		fvres	$⊢ k \in ℤ_{\geq i} \to ({(n \in Z ⟼ B) ↾}_{ℤ_{\geq i}}) (k) = (n \in Z ⟼ B) (k)$
114	113	adantl	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to ({(n \in Z ⟼ B) ↾}_{ℤ_{\geq i}}) (k) = (n \in Z ⟼ B) (k)$
115	112 114	eqtr3d	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to (n \in ℤ_{\geq i} ⟼ B) (k) = (n \in Z ⟼ B) (k)$
116	115	breq1d	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to ((n \in ℤ_{\geq i} ⟼ B) (k) \leq H (i) \leftrightarrow (n \in Z ⟼ B) (k) \leq H (i))$
117		eluzle	$⊢ k \in ℤ_{\geq i} \to i \leq k$
118	117	adantl	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to i \leq k$
119		biimt	$⊢ i \leq k \to ((n \in Z ⟼ B) (k) \leq H (i) \leftrightarrow (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i)))$
120	118 119	syl	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to ((n \in Z ⟼ B) (k) \leq H (i) \leftrightarrow (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i)))$
121	116 120	bitrd	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in ℤ_{\geq i}) \to ((n \in ℤ_{\geq i} ⟼ B) (k) \leq H (i) \leftrightarrow (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i)))$
122	121	ralbidva	$⊢ ((φ \land x \in A) \land i \in Z) \to (\forall k \in ℤ_{\geq i} (n \in ℤ_{\geq i} ⟼ B) (k) \leq H (i) \leftrightarrow \forall k \in ℤ_{\geq i} (i \leq k \to (n \in Z ⟼ B) (k) \leq H (i)))$
123	109 122	mpbird	$⊢ ((φ \land x \in A) \land i \in Z) \to \forall k \in ℤ_{\geq i} (n \in ℤ_{\geq i} ⟼ B) (k) \leq H (i)$
124		ffn	$⊢ (n \in ℤ_{\geq i} ⟼ B) : ℤ_{\geq i} ⟶ ℝ \to (n \in ℤ_{\geq i} ⟼ B) Fn ℤ_{\geq i}$
125		breq1	$⊢ z = (n \in ℤ_{\geq i} ⟼ B) (k) \to (z \leq H (i) \leftrightarrow (n \in ℤ_{\geq i} ⟼ B) (k) \leq H (i))$
126	125	ralrn	$⊢ (n \in ℤ_{\geq i} ⟼ B) Fn ℤ_{\geq i} \to (\forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq H (i) \leftrightarrow \forall k \in ℤ_{\geq i} (n \in ℤ_{\geq i} ⟼ B) (k) \leq H (i))$
127	80 124 126	3syl	$⊢ ((φ \land x \in A) \land i \in Z) \to (\forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq H (i) \leftrightarrow \forall k \in ℤ_{\geq i} (n \in ℤ_{\geq i} ⟼ B) (k) \leq H (i))$
128	123 127	mpbird	$⊢ ((φ \land x \in A) \land i \in Z) \to \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq H (i)$
129		brralrspcev	$⊢ (H (i) \in ℝ \land \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq H (i)) \to \exists y \in ℝ \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq y$
130	73 128 129	syl2anc	$⊢ ((φ \land x \in A) \land i \in Z) \to \exists y \in ℝ \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq y$
131	81 95 130	suprcld	$⊢ ((φ \land x \in A) \land i \in Z) \to sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \in ℝ$
132	131	rexrd	$⊢ ((φ \land x \in A) \land i \in Z) \to sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \in ℝ^{*}$
133	81	adantr	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to ran (n \in ℤ_{\geq i} ⟼ B) \subseteq ℝ$
134	95	adantr	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to ran (n \in ℤ_{\geq i} ⟼ B) \neq \emptyset$
135	130	adantr	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to \exists y \in ℝ \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq y$
136	12	sseli	$⊢ k \in Z \to k \in ℤ$
137		eluz	$⊢ (i \in ℤ \land k \in ℤ) \to (k \in ℤ_{\geq i} \leftrightarrow i \leq k)$
138	88 136 137	syl2an	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in Z) \to (k \in ℤ_{\geq i} \leftrightarrow i \leq k)$
139	138	biimprd	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in Z) \to (i \leq k \to k \in ℤ_{\geq i})$
140	139	impr	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to k \in ℤ_{\geq i}$
141	140 115	syldan	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to (n \in ℤ_{\geq i} ⟼ B) (k) = (n \in Z ⟼ B) (k)$
142	80	adantr	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to (n \in ℤ_{\geq i} ⟼ B) : ℤ_{\geq i} ⟶ ℝ$
143	142 124	syl	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to (n \in ℤ_{\geq i} ⟼ B) Fn ℤ_{\geq i}$
144		fnfvelrn	$⊢ ((n \in ℤ_{\geq i} ⟼ B) Fn ℤ_{\geq i} \land k \in ℤ_{\geq i}) \to (n \in ℤ_{\geq i} ⟼ B) (k) \in ran (n \in ℤ_{\geq i} ⟼ B)$
145	143 140 144	syl2anc	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to (n \in ℤ_{\geq i} ⟼ B) (k) \in ran (n \in ℤ_{\geq i} ⟼ B)$
146	141 145	eqeltrrd	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to (n \in Z ⟼ B) (k) \in ran (n \in ℤ_{\geq i} ⟼ B)$
147	133 134 135 146	suprubd	$⊢ (((φ \land x \in A) \land i \in Z) \land (k \in Z \land i \leq k)) \to (n \in Z ⟼ B) (k) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)$
148	147	expr	$⊢ (((φ \land x \in A) \land i \in Z) \land k \in Z) \to (i \leq k \to (n \in Z ⟼ B) (k) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
149	148	ralrimiva	$⊢ ((φ \land x \in A) \land i \in Z) \to \forall k \in Z (i \leq k \to (n \in Z ⟼ B) (k) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
150	3	limsupgle	$⊢ ((Z \subseteq ℝ \land (n \in Z ⟼ B) : Z ⟶ ℝ^{}) \land i \in ℝ \land sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \in ℝ^{}) \to (H (i) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \leftrightarrow \forall k \in Z (i \leq k \to (n \in Z ⟼ B) (k) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)))$
151	101 102 104 132 150	syl211anc	$⊢ ((φ \land x \in A) \land i \in Z) \to (H (i) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \leftrightarrow \forall k \in Z (i \leq k \to (n \in Z ⟼ B) (k) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)))$
152	149 151	mpbird	$⊢ ((φ \land x \in A) \land i \in Z) \to H (i) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)$
153		suprleub	$⊢ ((ran (n \in ℤ_{\geq i} ⟼ B) \subseteq ℝ \land ran (n \in ℤ_{\geq i} ⟼ B) \neq \emptyset \land \exists y \in ℝ \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq y) \land H (i) \in ℝ) \to (sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \leq H (i) \leftrightarrow \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq H (i))$
154	81 95 130 73 153	syl31anc	$⊢ ((φ \land x \in A) \land i \in Z) \to (sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \leq H (i) \leftrightarrow \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq H (i))$
155	128 154	mpbird	$⊢ ((φ \land x \in A) \land i \in Z) \to sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \leq H (i)$
156	74 132 152 155	xrletrid	$⊢ ((φ \land x \in A) \land i \in Z) \to H (i) = sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)$
157	156	mpteq2dva	$⊢ (φ \land x \in A) \to (i \in Z ⟼ H (i)) = (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
158	70 157	eqtrd	$⊢ (φ \land x \in A) \to {H ↾}_{Z} = (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
159	158	rneqd	$⊢ (φ \land x \in A) \to ran ({H ↾}_{Z}) = ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
160	65 159	syl5eq	$⊢ (φ \land x \in A) \to H [Z] = ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
161	160	infeq1d	$⊢ (φ \land x \in A) \to sup (H [Z] ℝ <) = sup (ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) ℝ <)$
162	19 64 161	3eqtrd	$⊢ (φ \land x \in A) \to lim sup ((n \in Z ⟼ B)) = sup (ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) ℝ <)$
163	162	mpteq2dva	$⊢ φ \to (x \in A ⟼ lim sup ((n \in Z ⟼ B))) = (x \in A ⟼ sup (ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) ℝ <))$
164	2 163	syl5eq	$⊢ φ \to G = (x \in A ⟼ sup (ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) ℝ <))$
165		eqid	$⊢ (x \in A ⟼ sup (ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) ℝ <)) = (x \in A ⟼ sup (ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) ℝ <))$
166		eqid	$⊢ ℤ_{\geq i} = ℤ_{\geq i}$
167		eqid	$⊢ (x \in A ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) = (x \in A ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
168		simpll	$⊢ ((φ \land i \in Z) \land n \in ℤ_{\geq i}) \to φ$
169	76	adantll	$⊢ ((φ \land i \in Z) \land n \in ℤ_{\geq i}) \to n \in Z$
170	168 169 6	syl2anc	$⊢ ((φ \land i \in Z) \land n \in ℤ_{\geq i}) \to (x \in A ⟼ B) \in MblFn$
171		simpll	$⊢ ((φ \land i \in Z) \land (n \in ℤ_{\geq i} \land x \in A)) \to φ$
172	76	ad2ant2lr	$⊢ ((φ \land i \in Z) \land (n \in ℤ_{\geq i} \land x \in A)) \to n \in Z$
173		simprr	$⊢ ((φ \land i \in Z) \land (n \in ℤ_{\geq i} \land x \in A)) \to x \in A$
174	171 172 173 7	syl12anc	$⊢ ((φ \land i \in Z) \land (n \in ℤ_{\geq i} \land x \in A)) \to B \in ℝ$
175	79	ralrimiva	$⊢ ((φ \land x \in A) \land i \in Z) \to \forall n \in ℤ_{\geq i} B \in ℝ$
176		breq1	$⊢ z = B \to (z \leq y \leftrightarrow B \leq y)$
177	82 176	ralrnmptw	$⊢ \forall n \in ℤ_{\geq i} B \in ℝ \to (\forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq y \leftrightarrow \forall n \in ℤ_{\geq i} B \leq y)$
178	175 177	syl	$⊢ ((φ \land x \in A) \land i \in Z) \to (\forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq y \leftrightarrow \forall n \in ℤ_{\geq i} B \leq y)$
179	178	rexbidv	$⊢ ((φ \land x \in A) \land i \in Z) \to (\exists y \in ℝ \forall z \in ran (n \in ℤ_{\geq i} ⟼ B) z \leq y \leftrightarrow \exists y \in ℝ \forall n \in ℤ_{\geq i} B \leq y)$
180	130 179	mpbid	$⊢ ((φ \land x \in A) \land i \in Z) \to \exists y \in ℝ \forall n \in ℤ_{\geq i} B \leq y$
181	180	an32s	$⊢ ((φ \land i \in Z) \land x \in A) \to \exists y \in ℝ \forall n \in ℤ_{\geq i} B \leq y$
182	166 167 87 170 174 181	mbfsup	$⊢ (φ \land i \in Z) \to (x \in A ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) \in MblFn$
183	131	an32s	$⊢ ((φ \land i \in Z) \land x \in A) \to sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \in ℝ$
184	183	anasss	$⊢ (φ \land (i \in Z \land x \in A)) \to sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \in ℝ$
185	3	limsuple	$⊢ (Z \subseteq ℝ \land (n \in Z ⟼ B) : Z ⟶ ℝ^{} \land lim sup ((n \in Z ⟼ B)) \in ℝ^{}) \to (lim sup ((n \in Z ⟼ B)) \leq lim sup ((n \in Z ⟼ B)) \leftrightarrow \forall i \in ℝ lim sup ((n \in Z ⟼ B)) \leq H (i))$
186	15 45 46 185	syl3anc	$⊢ (φ \land x \in A) \to (lim sup ((n \in Z ⟼ B)) \leq lim sup ((n \in Z ⟼ B)) \leftrightarrow \forall i \in ℝ lim sup ((n \in Z ⟼ B)) \leq H (i))$
187	43 186	mpbid	$⊢ (φ \land x \in A) \to \forall i \in ℝ lim sup ((n \in Z ⟼ B)) \leq H (i)$
188		ssralv	$⊢ Z \subseteq ℝ \to (\forall i \in ℝ lim sup ((n \in Z ⟼ B)) \leq H (i) \to \forall i \in Z lim sup ((n \in Z ⟼ B)) \leq H (i))$
189	14 187 188	mpsyl	$⊢ (φ \land x \in A) \to \forall i \in Z lim sup ((n \in Z ⟼ B)) \leq H (i)$
190	156	breq2d	$⊢ ((φ \land x \in A) \land i \in Z) \to (lim sup ((n \in Z ⟼ B)) \leq H (i) \leftrightarrow lim sup ((n \in Z ⟼ B)) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
191	190	ralbidva	$⊢ (φ \land x \in A) \to (\forall i \in Z lim sup ((n \in Z ⟼ B)) \leq H (i) \leftrightarrow \forall i \in Z lim sup ((n \in Z ⟼ B)) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
192	189 191	mpbid	$⊢ (φ \land x \in A) \to \forall i \in Z lim sup ((n \in Z ⟼ B)) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)$
193		breq1	$⊢ y = lim sup ((n \in Z ⟼ B)) \to (y \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \leftrightarrow lim sup ((n \in Z ⟼ B)) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
194	193	ralbidv	$⊢ y = lim sup ((n \in Z ⟼ B)) \to (\forall i \in Z y \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <) \leftrightarrow \forall i \in Z lim sup ((n \in Z ⟼ B)) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <))$
195	194	rspcev	$⊢ (lim sup ((n \in Z ⟼ B)) \in ℝ \land \forall i \in Z lim sup ((n \in Z ⟼ B)) \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) \to \exists y \in ℝ \forall i \in Z y \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)$
196	5 192 195	syl2anc	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall i \in Z y \leq sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)$
197	1 165 4 182 184 196	mbfinf	$⊢ φ \to (x \in A ⟼ sup (ran (i \in Z ⟼ sup (ran (n \in ℤ_{\geq i} ⟼ B) ℝ <)) ℝ <)) \in MblFn$
198	164 197	eqeltrd	$⊢ φ \to G \in MblFn$

Metamath Proof Explorer

Theorem mbflimsup

Proof