Theorem limsuppnfdlem

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	limsuppnfdlem.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	limsuppnfdlem.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
	limsuppnfdlem.u	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
	limsuppnfdlem.g	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion	limsuppnfdlem	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = +∞ )

Proof

Step	Hyp	Ref	Expression
1		limsuppnfdlem.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		limsuppnfdlem.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
3		limsuppnfdlem.u	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
4		limsuppnfdlem.g	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
5		reex	⊢ ℝ ∈ V
6	5	a1i	⊢ ( 𝜑 → ℝ ∈ V )
7	6 1	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
8	2 7	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
9	4	limsupval	⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
10	8 9	syl	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
11	2	ffund	⊢ ( 𝜑 → Fun 𝐹 )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → Fun 𝐹 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
14	2	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → dom 𝐹 = 𝐴 )
16	13 15	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ dom 𝐹 )
17	12 16	jca	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹 ) )
18	17	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹 ) )
19		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ∈ ℝ )
20	19	rexrd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ∈ ℝ* )
21		pnfxr	⊢ +∞ ∈ ℝ*
22	21	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → +∞ ∈ ℝ* )
23	1	ssrexr	⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
24	23	sselda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ℝ* )
25	24	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ℝ* )
26		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑘 ≤ 𝑗 )
27	1	sselda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ℝ )
28	27	ltpnfd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 < +∞ )
29	28	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑗 < +∞ )
30	20 22 25 26 29	elicod	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → 𝑗 ∈ ( 𝑘 [,) +∞ ) )
31		funfvima	⊢ ( ( Fun 𝐹 ∧ 𝑗 ∈ dom 𝐹 ) → ( 𝑗 ∈ ( 𝑘 [,) +∞ ) → ( 𝐹 ‘ 𝑗 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) )
32	18 30 31	sylc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
33	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
34	33	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
35	32 34	elind	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
36	35	adantllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
37	36	adantrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
38		simprr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
39		breq2	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑗 ) → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
40	39	rspcev	⊢ ( ( ( 𝐹 ‘ 𝑗 ) ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝑦 )
41	37 38 40	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝑦 )
42	3	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
43	42	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
44	43	an32s	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
45	41 44	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝑦 )
46	45	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝑦 )
47		inss2	⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
48		supxrunb3	⊢ ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝑦 ↔ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = +∞ ) )
49	47 48	mp1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝑦 ↔ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = +∞ ) )
50	46 49	mpbid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = +∞ )
51	50	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ +∞ ) )
52	4 51	syl5eq	⊢ ( 𝜑 → 𝐺 = ( 𝑘 ∈ ℝ ↦ +∞ ) )
53	52	rneqd	⊢ ( 𝜑 → ran 𝐺 = ran ( 𝑘 ∈ ℝ ↦ +∞ ) )
54		eqid	⊢ ( 𝑘 ∈ ℝ ↦ +∞ ) = ( 𝑘 ∈ ℝ ↦ +∞ )
55		ren0	⊢ ℝ ≠ ∅
56	55	a1i	⊢ ( 𝜑 → ℝ ≠ ∅ )
57	54 56	rnmptc	⊢ ( 𝜑 → ran ( 𝑘 ∈ ℝ ↦ +∞ ) = { +∞ } )
58	53 57	eqtrd	⊢ ( 𝜑 → ran 𝐺 = { +∞ } )
59	58	infeq1d	⊢ ( 𝜑 → inf ( ran 𝐺 , ℝ* , < ) = inf ( { +∞ } , ℝ* , < ) )
60		xrltso	⊢ < Or ℝ*
61		infsn	⊢ ( ( < Or ℝ* ∧ +∞ ∈ ℝ* ) → inf ( { +∞ } , ℝ* , < ) = +∞ )
62	60 21 61	mp2an	⊢ inf ( { +∞ } , ℝ* , < ) = +∞
63	62	a1i	⊢ ( 𝜑 → inf ( { +∞ } , ℝ* , < ) = +∞ )
64	10 59 63	3eqtrd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = +∞ )