supicclub2

Description: The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019)

Step	Hyp	Ref	Expression
1		supicc.1	$⊢ φ \to B \in ℝ$
2		supicc.2	$⊢ φ \to C \in ℝ$
3		supicc.3	$⊢ φ \to A \subseteq [B, C]$
4		supicc.4	$⊢ φ \to A \neq \emptyset$
5		supiccub.1	$⊢ φ \to D \in A$
6		supicclub2.1	$⊢ (φ \land z \in A) \to z \leq D$
7		iccssxr	$⊢ [B, C] \subseteq ℝ^{*}$
8	1 2 3 4	supicc	$⊢ φ \to sup (A ℝ <) \in [B, C]$
9	7 8	sselid	$⊢ φ \to sup (A ℝ <) \in ℝ^{*}$
10	3 7	sstrdi	$⊢ φ \to A \subseteq ℝ^{*}$
11	10 5	sseldd	$⊢ φ \to D \in ℝ^{*}$
12	10	sselda	$⊢ (φ \land z \in A) \to z \in ℝ^{*}$
13	11	adantr	$⊢ (φ \land z \in A) \to D \in ℝ^{*}$
14	12 13	xrlenltd	$⊢ (φ \land z \in A) \to (z \leq D \leftrightarrow \neg D < z)$
15	6 14	mpbid	$⊢ (φ \land z \in A) \to \neg D < z$
16	15	nrexdv	$⊢ φ \to \neg \exists z \in A D < z$
17	1 2 3 4 5	supicclub	$⊢ φ \to (D < sup (A ℝ <) \leftrightarrow \exists z \in A D < z)$
18	16 17	mtbird	$⊢ φ \to \neg D < sup (A ℝ <)$
19	9 11 18	xrnltled	$⊢ φ \to sup (A ℝ <) \leq D$

Metamath Proof Explorer