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 \subseteq ℝ \land A \in Fin) \to \exists x \in ℝ \forall y \in A x \leq y$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ A = \emptyset \to 0 \in ℝ$
2		rzal	$⊢ A = \emptyset \to \forall y \in A 0 \leq y$
3		breq1	$⊢ x = 0 \to (x \leq y \leftrightarrow 0 \leq y)$
4	3	ralbidv	$⊢ x = 0 \to (\forall y \in A x \leq y \leftrightarrow \forall y \in A 0 \leq y)$
5	4	rspcev	$⊢ (0 \in ℝ \land \forall y \in A 0 \leq y) \to \exists x \in ℝ \forall y \in A x \leq y$
6	1 2 5	syl2anc	$⊢ A = \emptyset \to \exists x \in ℝ \forall y \in A x \leq y$
7	6	adantl	$⊢ ((A \subseteq ℝ \land A \in Fin) \land A = \emptyset) \to \exists x \in ℝ \forall y \in A x \leq y$
8		neqne	$⊢ \neg A = \emptyset \to A \neq \emptyset$
9	8	adantl	$⊢ ((A \subseteq ℝ \land A \in Fin) \land \neg A = \emptyset) \to A \neq \emptyset$
10		simpll	$⊢ ((A \subseteq ℝ \land A \in Fin) \land A \neq \emptyset) \to A \subseteq ℝ$
11		simplr	$⊢ ((A \subseteq ℝ \land A \in Fin) \land A \neq \emptyset) \to A \in Fin$
12		simpr	$⊢ ((A \subseteq ℝ \land A \in Fin) \land A \neq \emptyset) \to A \neq \emptyset$
13		fiminre	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A x \leq y$
14	10 11 12 13	syl3anc	$⊢ ((A \subseteq ℝ \land A \in Fin) \land A \neq \emptyset) \to \exists x \in A \forall y \in A x \leq y$
15		ssrexv	$⊢ A \subseteq ℝ \to (\exists x \in A \forall y \in A x \leq y \to \exists x \in ℝ \forall y \in A x \leq y)$
16	10 14 15	sylc	$⊢ ((A \subseteq ℝ \land A \in Fin) \land A \neq \emptyset) \to \exists x \in ℝ \forall y \in A x \leq y$
17	9 16	syldan	$⊢ ((A \subseteq ℝ \land A \in Fin) \land \neg A = \emptyset) \to \exists x \in ℝ \forall y \in A x \leq y$
18	7 17	pm2.61dan	$⊢ (A \subseteq ℝ \land A \in Fin) \to \exists x \in ℝ \forall y \in A x \leq y$