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 = ( ZZ>= ` M )
	mbflimsup.2	\|- G = ( x e. A \|-> ( limsup ` ( n e. Z \|-> B ) ) )
	mbflimsup.h	\|- H = ( m e. RR \|-> sup ( ( ( ( n e. Z \|-> B ) " ( m [,) +oo ) ) i^i RR* ) , RR* , < ) )
	mbflimsup.3	\|- ( ph -> M e. ZZ )
	mbflimsup.4	\|- ( ( ph /\ x e. A ) -> ( limsup ` ( n e. Z \|-> B ) ) e. RR )
	mbflimsup.5	\|- ( ( ph /\ n e. Z ) -> ( x e. A \|-> B ) e. MblFn )
	mbflimsup.6	\|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
Assertion	mbflimsup	\|- ( ph -> G e. MblFn )

Proof

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

Metamath Proof Explorer

Theorem mbflimsup

Proof