Metamath Proof Explorer

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 ⊢F:M…N⟶ℝ→∃x∈ℝ∀y∈ran⁡Fy≤x

Proof

Step Hyp Ref Expression
1 fzfi ⊢M…N∈Fin
2 ffvelcdm ⊢F:M…N⟶ℝ∧k∈M…N→F⁡k∈ℝ
3 2 ralrimiva ⊢F:M…N⟶ℝ→∀k∈M…NF⁡k∈ℝ
4 fimaxre3 ⊢M…N∈Fin∧∀k∈M…NF⁡k∈ℝ→∃x∈ℝ∀k∈M…NF⁡k≤x
5 1 3 4 sylancr ⊢F:M…N⟶ℝ→∃x∈ℝ∀k∈M…NF⁡k≤x
6 ffn ⊢F:M…N⟶ℝ→FFnM…N
7 breq1 ⊢y=F⁡k→y≤x↔F⁡k≤x
8 7 ralrn ⊢FFnM…N→∀y∈ran⁡Fy≤x↔∀k∈M…NF⁡k≤x
9 6 8 syl ⊢F:M…N⟶ℝ→∀y∈ran⁡Fy≤x↔∀k∈M…NF⁡k≤x
10 9 rexbidv ⊢F:M…N⟶ℝ→∃x∈ℝ∀y∈ran⁡Fy≤x↔∃x∈ℝ∀k∈M…NF⁡k≤x
11 5 10 mpbird ⊢F:M…N⟶ℝ→∃x∈ℝ∀y∈ran⁡Fy≤x