Theorem 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		ffvelrn	|- ( ( 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	sseldi	|- ( ( ( 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	syl5eq	|- ( ( 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	syl5eq	|- ( 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 )