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