Theorem limsuppnfd

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	limsuppnfd.j	⊢ Ⅎ 𝑗 𝐹
	limsuppnfd.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	limsuppnfd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
	limsuppnfd.u	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
Assertion	limsuppnfd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = +∞ )

Proof

Step	Hyp	Ref	Expression
1		limsuppnfd.j	⊢ Ⅎ 𝑗 𝐹
2		limsuppnfd.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		limsuppnfd.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4		limsuppnfd.u	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
5		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
6	5	anbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
7	6	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
8		breq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 ≤ 𝑗 ↔ 𝑖 ≤ 𝑗 ) )
9	8	anbi1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
10	9	rexbidv	⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
11		nfv	⊢ Ⅎ 𝑙 ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) )
12		nfv	⊢ Ⅎ 𝑗 𝑖 ≤ 𝑙
13		nfcv	⊢ Ⅎ 𝑗 𝑦
14		nfcv	⊢ Ⅎ 𝑗 ≤
15		nfcv	⊢ Ⅎ 𝑗 𝑙
16	1 15	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
17	13 14 16	nfbr	⊢ Ⅎ 𝑗 𝑦 ≤ ( 𝐹 ‘ 𝑙 )
18	12 17	nfan	⊢ Ⅎ 𝑗 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) )
19		breq2	⊢ ( 𝑗 = 𝑙 → ( 𝑖 ≤ 𝑗 ↔ 𝑖 ≤ 𝑙 ) )
20		fveq2	⊢ ( 𝑗 = 𝑙 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑙 ) )
21	20	breq2d	⊢ ( 𝑗 = 𝑙 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
22	19 21	anbi12d	⊢ ( 𝑗 = 𝑙 → ( ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
23	11 18 22	cbvrexw	⊢ ( ∃ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
24	23	a1i	⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
25	10 24	bitrd	⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
26	7 25	cbvral2vw	⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
27	4 26	sylib	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
28		eqid	⊢ ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
29	2 3 27 28	limsuppnfdlem	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = +∞ )