Theorem limsupmnf

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupmnf.j	⊢ Ⅎ 𝑗 𝐹
	limsupmnf.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	limsupmnf.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
Assertion	limsupmnf	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupmnf.j	⊢ Ⅎ 𝑗 𝐹
2		limsupmnf.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		limsupmnf.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4		eqid	⊢ ( 𝑖 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) , ℝ* , < ) )
5	2 3 4	limsupmnflem	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) )
6		breq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
7	6	imbi2d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
8	7	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
9	8	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
10		breq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 ≤ 𝑙 ↔ 𝑘 ≤ 𝑙 ) )
11	10	imbi1d	⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
12	11	ralbidv	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
13		nfv	⊢ Ⅎ 𝑗 𝑘 ≤ 𝑙
14		nfcv	⊢ Ⅎ 𝑗 𝑙
15	1 14	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
16		nfcv	⊢ Ⅎ 𝑗 ≤
17		nfcv	⊢ Ⅎ 𝑗 𝑥
18	15 16 17	nfbr	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
19	13 18	nfim	⊢ Ⅎ 𝑗 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
20		nfv	⊢ Ⅎ 𝑙 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
21		breq2	⊢ ( 𝑙 = 𝑗 → ( 𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑗 ) )
22		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
23	22	breq1d	⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
24	21 23	imbi12d	⊢ ( 𝑙 = 𝑗 → ( ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
25	19 20 24	cbvralw	⊢ ( ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
26	25	a1i	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
27	12 26	bitrd	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
28	27	cbvrexvw	⊢ ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
29	28	a1i	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
30	9 29	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
31	30	cbvralvw	⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
32	31	a1i	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
33	5 32	bitrd	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )