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

Metamath Proof Explorer

Theorem infxrlb

Description: A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014) (Revised by AV, 5-Sep-2020)

		Ref	Expression
	Assertion	infxrlb	$⊢ (A \subseteq ℝ^{} \land B \in A) \to inf (A ℝ^{} <) \leq B$

Proof

Step	Hyp	Ref	Expression
1		infxrcl	$⊢ A \subseteq ℝ^{} \to inf (A ℝ^{} <) \in ℝ^{*}$
2	1	adantr	$⊢ (A \subseteq ℝ^{} \land B \in A) \to inf (A ℝ^{} <) \in ℝ^{*}$
3		ssel2	$⊢ (A \subseteq ℝ^{} \land B \in A) \to B \in ℝ^{}$
4		xrltso	$⊢ < Or ℝ^{*}$
5	4	a1i	$⊢ A \subseteq ℝ^{} \to < Or ℝ^{}$
6		xrinfmss	$⊢ A \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y))$
7	5 6	inflb	$⊢ A \subseteq ℝ^{} \to (B \in A \to \neg B < inf (A ℝ^{} <))$
8	7	imp	$⊢ (A \subseteq ℝ^{} \land B \in A) \to \neg B < inf (A ℝ^{} <)$
9	2 3 8	xrnltled	$⊢ (A \subseteq ℝ^{} \land B \in A) \to inf (A ℝ^{} <) \leq B$