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

Metamath Proof Explorer

Theorem lbinf

Description: If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005) (Revised by AV, 4-Sep-2020)

		Ref	Expression
	Assertion	lbinf	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to inf (S ℝ <) = (ι x \in S \| \forall y \in S x \leq y)$

Proof

Step	Hyp	Ref	Expression
1		ltso	$⊢ < Or ℝ$
2	1	a1i	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to < Or ℝ$
3		lbcl	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to (ι x \in S \| \forall y \in S x \leq y) \in S$
4		ssel	$⊢ S \subseteq ℝ \to ((ι x \in S \| \forall y \in S x \leq y) \in S \to (ι x \in S \| \forall y \in S x \leq y) \in ℝ)$
5	4	adantr	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to ((ι x \in S \| \forall y \in S x \leq y) \in S \to (ι x \in S \| \forall y \in S x \leq y) \in ℝ)$
6	3 5	mpd	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to (ι x \in S \| \forall y \in S x \leq y) \in ℝ$
7	6	adantr	$⊢ ((S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \land z \in S) \to (ι x \in S \| \forall y \in S x \leq y) \in ℝ$
8		ssel2	$⊢ (S \subseteq ℝ \land z \in S) \to z \in ℝ$
9	8	adantlr	$⊢ ((S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \land z \in S) \to z \in ℝ$
10		lble	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y \land z \in S) \to (ι x \in S \| \forall y \in S x \leq y) \leq z$
11	10	3expa	$⊢ ((S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \land z \in S) \to (ι x \in S \| \forall y \in S x \leq y) \leq z$
12	7 9 11	lensymd	$⊢ ((S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \land z \in S) \to \neg z < (ι x \in S \| \forall y \in S x \leq y)$
13	2 6 3 12	infmin	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to inf (S ℝ <) = (ι x \in S \| \forall y \in S x \leq y)$