Theorem limsuppnf

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsuppnf.j	|- F/_ j F
	limsuppnf.a	|- ( ph -> A C_ RR )
	limsuppnf.f	|- ( ph -> F : A --> RR* )
Assertion	limsuppnf	|- ( ph -> ( ( limsup ` F ) = +oo <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsuppnf.j	|- F/_ j F
2		limsuppnf.a	|- ( ph -> A C_ RR )
3		limsuppnf.f	|- ( ph -> F : A --> RR* )
4		nfcv	|- F/_ l F
5	4 2 3	limsuppnflem	|- ( ph -> ( ( limsup ` F ) = +oo <-> A. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) ) )
6		breq1	|- ( i = k -> ( i <_ l <-> k <_ l ) )
7	6	anbi1d	|- ( i = k -> ( ( i <_ l /\ y <_ ( F ` l ) ) <-> ( k <_ l /\ y <_ ( F ` l ) ) ) )
8	7	rexbidv	|- ( i = k -> ( E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> E. l e. A ( k <_ l /\ y <_ ( F ` l ) ) ) )
9		nfv	|- F/ j k <_ l
10		nfcv	|- F/_ j y
11		nfcv	|- F/_ j <_
12		nfcv	|- F/_ j l
13	1 12	nffv	|- F/_ j ( F ` l )
14	10 11 13	nfbr	|- F/ j y <_ ( F ` l )
15	9 14	nfan	|- F/ j ( k <_ l /\ y <_ ( F ` l ) )
16		nfv	|- F/ l ( k <_ j /\ y <_ ( F ` j ) )
17		breq2	|- ( l = j -> ( k <_ l <-> k <_ j ) )
18		fveq2	|- ( l = j -> ( F ` l ) = ( F ` j ) )
19	18	breq2d	|- ( l = j -> ( y <_ ( F ` l ) <-> y <_ ( F ` j ) ) )
20	17 19	anbi12d	|- ( l = j -> ( ( k <_ l /\ y <_ ( F ` l ) ) <-> ( k <_ j /\ y <_ ( F ` j ) ) ) )
21	15 16 20	cbvrexw	|- ( E. l e. A ( k <_ l /\ y <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) )
22	21	a1i	|- ( i = k -> ( E. l e. A ( k <_ l /\ y <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
23	8 22	bitrd	|- ( i = k -> ( E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
24	23	cbvralvw	|- ( A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) )
25	24	a1i	|- ( y = x -> ( A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
26		breq1	|- ( y = x -> ( y <_ ( F ` j ) <-> x <_ ( F ` j ) ) )
27	26	anbi2d	|- ( y = x -> ( ( k <_ j /\ y <_ ( F ` j ) ) <-> ( k <_ j /\ x <_ ( F ` j ) ) ) )
28	27	rexbidv	|- ( y = x -> ( E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) <-> E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
29	28	ralbidv	|- ( y = x -> ( A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
30	25 29	bitrd	|- ( y = x -> ( A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
31	30	cbvralvw	|- ( A. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
32	31	a1i	|- ( ph -> ( A. y e. RR A. i e. RR E. l e. A ( i <_ l /\ y <_ ( F ` l ) ) <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
33	5 32	bitrd	|- ( ph -> ( ( limsup ` F ) = +oo <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )