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

Proof

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