Metamath Proof Explorer

Theorem infmrgelbi

Description: Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013) (Revised by AV, 17-Sep-2020)

		Ref	Expression
	Assertion	infmrgelbi	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land B \in ℝ) \land \forall x \in A B \leq x) \to B \leq sup (A ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land B \in ℝ) \land \forall x \in A B \leq x) \to \forall x \in A B \leq x$
2		simpl1	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land B \in ℝ) \land \forall x \in A B \leq x) \to A \subseteq ℝ$
3		simpl2	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land B \in ℝ) \land \forall x \in A B \leq x) \to A \neq \emptyset$
4		breq1	$⊢ z = B \to (z \leq x \leftrightarrow B \leq x)$
5	4	ralbidv	$⊢ z = B \to (\forall x \in A z \leq x \leftrightarrow \forall x \in A B \leq x)$
6	5	rspcev	$⊢ (B \in ℝ \land \forall x \in A B \leq x) \to \exists z \in ℝ \forall x \in A z \leq x$
7	6	3ad2antl3	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land B \in ℝ) \land \forall x \in A B \leq x) \to \exists z \in ℝ \forall x \in A z \leq x$
8		simpl3	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land B \in ℝ) \land \forall x \in A B \leq x) \to B \in ℝ$
9		infregelb	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists z \in ℝ \forall x \in A z \leq x) \land B \in ℝ) \to (B \leq sup (A ℝ <) \leftrightarrow \forall x \in A B \leq x)$
10	2 3 7 8 9	syl31anc	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land B \in ℝ) \land \forall x \in A B \leq x) \to (B \leq sup (A ℝ <) \leftrightarrow \forall x \in A B \leq x)$
11	1 10	mpbird	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land B \in ℝ) \land \forall x \in A B \leq x) \to B \leq sup (A ℝ <)$