Metamath Proof Explorer

Theorem fimaxre2

Description: A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011) (Revised by Mario Carneiro, 13-Feb-2014)

Ref Expression
Assertion fimaxre2 ⊢ A ⊆ ℝ ∧ A ∈ Fin → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 rzal ⊢ A = ∅ → ∀ y ∈ A y ≤ 0
3 brralrspcev ⊢ 0 ∈ ℝ ∧ ∀ y ∈ A y ≤ 0 → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
4 1 2 3 sylancr ⊢ A = ∅ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
5 4 a1i ⊢ A ⊆ ℝ ∧ A ∈ Fin → A = ∅ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
6 fimaxre ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ A ≠ ∅ → ∃ x ∈ A ∀ y ∈ A y ≤ x
7 6 3expia ⊢ A ⊆ ℝ ∧ A ∈ Fin → A ≠ ∅ → ∃ x ∈ A ∀ y ∈ A y ≤ x
8 ssrexv ⊢ A ⊆ ℝ → ∃ x ∈ A ∀ y ∈ A y ≤ x → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
9 8 adantr ⊢ A ⊆ ℝ ∧ A ∈ Fin → ∃ x ∈ A ∀ y ∈ A y ≤ x → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
10 7 9 syld ⊢ A ⊆ ℝ ∧ A ∈ Fin → A ≠ ∅ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
11 5 10 pm2.61dne ⊢ A ⊆ ℝ ∧ A ∈ Fin → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x