Theorem limsupmnfuz

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 a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupmnfuz.1	⊢ Ⅎ 𝑗 𝐹
	limsupmnfuz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupmnfuz.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	limsupmnfuz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	limsupmnfuz	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		limsupmnfuz.1	⊢ Ⅎ 𝑗 𝐹
2		limsupmnfuz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupmnfuz.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		limsupmnfuz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
5	2 3 4	limsupmnfuzlem	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
6		breq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
7	6	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
8	7	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
9		fveq2	⊢ ( 𝑖 = 𝑘 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑘 ) )
10	9	raleqdv	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
11		nfcv	⊢ Ⅎ 𝑗 𝑙
12	1 11	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
13		nfcv	⊢ Ⅎ 𝑗 ≤
14		nfcv	⊢ Ⅎ 𝑗 𝑥
15	12 13 14	nfbr	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
16		nfv	⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
17		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
18	17	breq1d	⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
19	15 16 18	cbvralw	⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
20	19	a1i	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
21	10 20	bitrd	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
22	21	cbvrexvw	⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
23	22	a1i	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
24	8 23	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
25	24	cbvralvw	⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
26	25	a1i	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
27	5 26	bitrd	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )