Metamath Proof Explorer

Theorem fiminre2

Description: A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 0red ⊢ A = ∅ → 0 ∈ ℝ
2 rzal ⊢ A = ∅ → ∀ y ∈ A 0 ≤ y
3 breq1 ⊢ x = 0 → x ≤ y ↔ 0 ≤ y
4 3 ralbidv ⊢ x = 0 → ∀ y ∈ A x ≤ y ↔ ∀ y ∈ A 0 ≤ y
5 4 rspcev ⊢ 0 ∈ ℝ ∧ ∀ y ∈ A 0 ≤ y → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y
6 1 2 5 syl2anc ⊢ A = ∅ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y
7 6 adantl ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ A = ∅ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y
8 neqne ⊢ ¬ A = ∅ → A ≠ ∅
9 8 adantl ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ ¬ A = ∅ → A ≠ ∅
10 simpll ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ A ≠ ∅ → A ⊆ ℝ
11 simplr ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ A ≠ ∅ → A ∈ Fin
12 simpr ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ A ≠ ∅ → A ≠ ∅
13 fiminre ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ A ≠ ∅ → ∃ x ∈ A ∀ y ∈ A x ≤ y
14 10 11 12 13 syl3anc ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ A ≠ ∅ → ∃ x ∈ A ∀ y ∈ A x ≤ y
15 ssrexv ⊢ A ⊆ ℝ → ∃ x ∈ A ∀ y ∈ A x ≤ y → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y
16 10 14 15 sylc ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ A ≠ ∅ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y
17 9 16 syldan ⊢ A ⊆ ℝ ∧ A ∈ Fin ∧ ¬ A = ∅ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y
18 7 17 pm2.61dan ⊢ A ⊆ ℝ ∧ A ∈ Fin → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y