Metamath Proof Explorer

Theorem infxrge0lb

Description: A member of a set of nonnegative extended reals is greater than or equal to the set's infimum. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

		Ref	Expression
	Hypotheses	infxrge0lb.a	$⊢ φ \to A \subseteq [0, +∞]$
		infxrge0lb.b	$⊢ φ \to B \in A$
	Assertion	infxrge0lb	$⊢ φ \to sup (A [0, +∞] <) \leq B$

Proof

Step	Hyp	Ref	Expression
1		infxrge0lb.a	$⊢ φ \to A \subseteq [0, +∞]$
2		infxrge0lb.b	$⊢ φ \to B \in A$
3		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
4		xrltso	$⊢ < Or ℝ^{*}$
5		soss	$⊢ [0, +∞] \subseteq ℝ^{} \to (< Or ℝ^{} \to < Or [0, +∞])$
6	3 4 5	mp2	$⊢ < Or [0, +∞]$
7	6	a1i	$⊢ φ \to < Or [0, +∞]$
8		xrge0infss	$⊢ A \subseteq [0, +∞] \to \exists x \in [0, +∞] (\forall y \in A \neg y < x \land \forall y \in [0, +∞] (x < y \to \exists z \in A z < y))$
9	1 8	syl	$⊢ φ \to \exists x \in [0, +∞] (\forall y \in A \neg y < x \land \forall y \in [0, +∞] (x < y \to \exists z \in A z < y))$
10	7 9	infcl	$⊢ φ \to sup (A [0, +∞] <) \in [0, +∞]$
11	3 10	sselid	$⊢ φ \to sup (A [0, +∞] <) \in ℝ^{*}$
12	1 2	sseldd	$⊢ φ \to B \in [0, +∞]$
13	3 12	sselid	$⊢ φ \to B \in ℝ^{*}$
14	7 9	inflb	$⊢ φ \to (B \in A \to \neg B < sup (A [0, +∞] <))$
15	2 14	mpd	$⊢ φ \to \neg B < sup (A [0, +∞] <)$
16	11 13 15	xrnltled	$⊢ φ \to sup (A [0, +∞] <) \leq B$