Theorem limsuple

Description: The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypothesis	limsupval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion	limsuple	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑗 ∈ ℝ 𝐴 ≤ ( 𝐺 ‘ 𝑗 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2		simp2	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → 𝐹 : 𝐵 ⟶ ℝ* )
3		reex	⊢ ℝ ∈ V
4	3	ssex	⊢ ( 𝐵 ⊆ ℝ → 𝐵 ∈ V )
5	4	3ad2ant1	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → 𝐵 ∈ V )
6		xrex	⊢ ℝ* ∈ V
7	6	a1i	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ℝ* ∈ V )
8		fex2	⊢ ( ( 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐵 ∈ V ∧ ℝ* ∈ V ) → 𝐹 ∈ V )
9	2 5 7 8	syl3anc	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → 𝐹 ∈ V )
10	1	limsupval	⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
11	9 10	syl	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) )
12	11	breq2d	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ 𝐴 ≤ inf ( ran 𝐺 , ℝ* , < ) ) )
13	1	limsupgf	⊢ 𝐺 : ℝ ⟶ ℝ*
14		frn	⊢ ( 𝐺 : ℝ ⟶ ℝ* → ran 𝐺 ⊆ ℝ* )
15	13 14	ax-mp	⊢ ran 𝐺 ⊆ ℝ*
16		simp3	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
17		infxrgelb	⊢ ( ( ran 𝐺 ⊆ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ inf ( ran 𝐺 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 𝐴 ≤ 𝑥 ) )
18	15 16 17	sylancr	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ inf ( ran 𝐺 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 𝐴 ≤ 𝑥 ) )
19		ffn	⊢ ( 𝐺 : ℝ ⟶ ℝ* → 𝐺 Fn ℝ )
20	13 19	ax-mp	⊢ 𝐺 Fn ℝ
21		breq2	⊢ ( 𝑥 = ( 𝐺 ‘ 𝑗 ) → ( 𝐴 ≤ 𝑥 ↔ 𝐴 ≤ ( 𝐺 ‘ 𝑗 ) ) )
22	21	ralrn	⊢ ( 𝐺 Fn ℝ → ( ∀ 𝑥 ∈ ran 𝐺 𝐴 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℝ 𝐴 ≤ ( 𝐺 ‘ 𝑗 ) ) )
23	20 22	ax-mp	⊢ ( ∀ 𝑥 ∈ ran 𝐺 𝐴 ≤ 𝑥 ↔ ∀ 𝑗 ∈ ℝ 𝐴 ≤ ( 𝐺 ‘ 𝑗 ) )
24	18 23	bitrdi	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ inf ( ran 𝐺 , ℝ* , < ) ↔ ∀ 𝑗 ∈ ℝ 𝐴 ≤ ( 𝐺 ‘ 𝑗 ) ) )
25	12 24	bitrd	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑗 ∈ ℝ 𝐴 ≤ ( 𝐺 ‘ 𝑗 ) ) )