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

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 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )

Proof

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