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

Metamath Proof Explorer

Theorem infrglb

Description: The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Revised by AV, 15-Sep-2020)

		Ref	Expression
	Assertion	infrglb	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land B \in ℝ) \to (inf (A ℝ <) < B \leftrightarrow \exists z \in A z < B)$

Proof

Step	Hyp	Ref	Expression
1		ltso	$⊢ < Or ℝ$
2	1	a1i	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to < Or ℝ$
3		infm3	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to \exists x \in ℝ (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y))$
4		simp1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to A \subseteq ℝ$
5	2 3 4	infglbb	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \land B \in ℝ) \to (inf (A ℝ <) < B \leftrightarrow \exists z \in A z < B)$