This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fimaxre4

Description: A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses fimaxre4.1 ⊢ Ⅎ x φ
fimaxre4.2 ⊢ φ → A ∈ Fin
fimaxre4.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ
Assertion fimaxre4 ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y

Proof

Step Hyp Ref Expression
1 fimaxre4.1 ⊢ Ⅎ x φ
2 fimaxre4.2 ⊢ φ → A ∈ Fin
3 fimaxre4.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ
4 3 ex ⊢ φ → x ∈ A → B ∈ ℝ
5 1 4 ralrimi ⊢ φ → ∀ x ∈ A B ∈ ℝ
6 fimaxre3 ⊢ A ∈ Fin ∧ ∀ x ∈ A B ∈ ℝ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
7 2 5 6 syl2anc ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y