lbreu

Description: If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005)

		Ref	Expression
	Assertion	lbreu	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to \exists! x \in S \forall y \in S x \leq y$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ y = w \to (x \leq y \leftrightarrow x \leq w)$
2	1	rspcv	$⊢ w \in S \to (\forall y \in S x \leq y \to x \leq w)$
3		breq2	$⊢ y = x \to (w \leq y \leftrightarrow w \leq x)$
4	3	rspcv	$⊢ x \in S \to (\forall y \in S w \leq y \to w \leq x)$
5	2 4	im2anan9r	$⊢ (x \in S \land w \in S) \to ((\forall y \in S x \leq y \land \forall y \in S w \leq y) \to (x \leq w \land w \leq x))$
6		ssel	$⊢ S \subseteq ℝ \to (x \in S \to x \in ℝ)$
7		ssel	$⊢ S \subseteq ℝ \to (w \in S \to w \in ℝ)$
8	6 7	anim12d	$⊢ S \subseteq ℝ \to ((x \in S \land w \in S) \to (x \in ℝ \land w \in ℝ))$
9	8	impcom	$⊢ ((x \in S \land w \in S) \land S \subseteq ℝ) \to (x \in ℝ \land w \in ℝ)$
10		letri3	$⊢ (x \in ℝ \land w \in ℝ) \to (x = w \leftrightarrow (x \leq w \land w \leq x))$
11	9 10	syl	$⊢ ((x \in S \land w \in S) \land S \subseteq ℝ) \to (x = w \leftrightarrow (x \leq w \land w \leq x))$
12	11	exbiri	$⊢ (x \in S \land w \in S) \to (S \subseteq ℝ \to ((x \leq w \land w \leq x) \to x = w))$
13	12	com23	$⊢ (x \in S \land w \in S) \to ((x \leq w \land w \leq x) \to (S \subseteq ℝ \to x = w))$
14	5 13	syld	$⊢ (x \in S \land w \in S) \to ((\forall y \in S x \leq y \land \forall y \in S w \leq y) \to (S \subseteq ℝ \to x = w))$
15	14	com3r	$⊢ S \subseteq ℝ \to ((x \in S \land w \in S) \to ((\forall y \in S x \leq y \land \forall y \in S w \leq y) \to x = w))$
16	15	ralrimivv	$⊢ S \subseteq ℝ \to \forall x \in S \forall w \in S ((\forall y \in S x \leq y \land \forall y \in S w \leq y) \to x = w)$
17	16	anim1ci	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to (\exists x \in S \forall y \in S x \leq y \land \forall x \in S \forall w \in S ((\forall y \in S x \leq y \land \forall y \in S w \leq y) \to x = w))$
18		breq1	$⊢ x = w \to (x \leq y \leftrightarrow w \leq y)$
19	18	ralbidv	$⊢ x = w \to (\forall y \in S x \leq y \leftrightarrow \forall y \in S w \leq y)$
20	19	reu4	$⊢ \exists! x \in S \forall y \in S x \leq y \leftrightarrow (\exists x \in S \forall y \in S x \leq y \land \forall x \in S \forall w \in S ((\forall y \in S x \leq y \land \forall y \in S w \leq y) \to x = w))$
21	17 20	sylibr	$⊢ (S \subseteq ℝ \land \exists x \in S \forall y \in S x \leq y) \to \exists! x \in S \forall y \in S x \leq y$

Metamath Proof Explorer

Theorem lbreu

Proof