Metamath Proof Explorer

Theorem ubelsupr

Description: If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017)

		Ref	Expression
	Assertion	ubelsupr	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to U = sup (A ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to A \subseteq ℝ$
2		simp2	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to U \in A$
3	2	ne0d	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to A \neq \emptyset$
4	1 2	sseldd	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to U \in ℝ$
5		simp3	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to \forall x \in A x \leq U$
6		brralrspcev	$⊢ (U \in ℝ \land \forall x \in A x \leq U) \to \exists y \in ℝ \forall x \in A x \leq y$
7	4 5 6	syl2anc	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to \exists y \in ℝ \forall x \in A x \leq y$
8	1 3 7	3jca	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to (A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y)$
9		suprub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y) \land U \in A) \to U \leq sup (A ℝ <)$
10	8 2 9	syl2anc	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to U \leq sup (A ℝ <)$
11		suprleub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y) \land U \in ℝ) \to (sup (A ℝ <) \leq U \leftrightarrow \forall x \in A x \leq U)$
12	8 4 11	syl2anc	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to (sup (A ℝ <) \leq U \leftrightarrow \forall x \in A x \leq U)$
13	5 12	mpbird	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to sup (A ℝ <) \leq U$
14		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y) \to sup (A ℝ <) \in ℝ$
15	8 14	syl	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to sup (A ℝ <) \in ℝ$
16	4 15	letri3d	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to (U = sup (A ℝ <) \leftrightarrow (U \leq sup (A ℝ <) \land sup (A ℝ <) \leq U))$
17	10 13 16	mpbir2and	$⊢ (A \subseteq ℝ \land U \in A \land \forall x \in A x \leq U) \to U = sup (A ℝ <)$