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

Metamath Proof Explorer

Theorem infxrglb

Description: The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Assertion	infxrglb	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (inf (A ℝ^{*} <) < B \leftrightarrow \exists x \in A x < B)$

Proof

Step	Hyp	Ref	Expression
1		xrltso	$⊢ < Or ℝ^{*}$
2	1	a1i	$⊢ A \subseteq ℝ^{} \to < Or ℝ^{}$
3		xrinfmss	$⊢ A \subseteq ℝ^{} \to \exists z \in ℝ^{} (\forall y \in A \neg y < z \land \forall y \in ℝ^{*} (z < y \to \exists x \in A x < y))$
4		id	$⊢ A \subseteq ℝ^{} \to A \subseteq ℝ^{}$
5	2 3 4	infglbb	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (inf (A ℝ^{*} <) < B \leftrightarrow \exists x \in A x < B)$