Theorem fsequb2

Description: The values of a finite real sequence have an upper bound. (Contributed by NM, 20-Sep-2005) (Proof shortened by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fsequb2	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		fzfi	⊢ ( 𝑀 ... 𝑁 ) ∈ Fin
2		ffvelcdm	⊢ ( ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
3	2	ralrimiva	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
4		fimaxre3	⊢ ( ( ( 𝑀 ... 𝑁 ) ∈ Fin ∧ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
5	1 3 4	sylancr	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
6		ffn	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → 𝐹 Fn ( 𝑀 ... 𝑁 ) )
7		breq1	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( 𝑦 ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
8	7	ralrn	⊢ ( 𝐹 Fn ( 𝑀 ... 𝑁 ) → ( ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
9	6 8	syl	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ( ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
10	9	rexbidv	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
11	5 10	mpbird	⊢ ( 𝐹 : ( 𝑀 ... 𝑁 ) ⟶ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )