supicc

Description: Supremum of a bounded set of real numbers. (Contributed by Thierry Arnoux, 17-May-2019)

	Ref	Expression
Hypotheses	supicc.1	$⊢ φ \to B \in ℝ$
	supicc.2	$⊢ φ \to C \in ℝ$
	supicc.3	$⊢ φ \to A \subseteq [B, C]$
	supicc.4	$⊢ φ \to A \neq \emptyset$
Assertion	supicc	$⊢ φ \to sup (A ℝ <) \in [B, C]$

Proof

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		iccssre	$⊢ (B \in ℝ \land C \in ℝ) \to [B, C] \subseteq ℝ$
6	1 2 5	syl2anc	$⊢ φ \to [B, C] \subseteq ℝ$
7	3 6	sstrd	$⊢ φ \to A \subseteq ℝ$
8	1	adantr	$⊢ (φ \land x \in A) \to B \in ℝ$
9	8	rexrd	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
10	2	adantr	$⊢ (φ \land x \in A) \to C \in ℝ$
11	10	rexrd	$⊢ (φ \land x \in A) \to C \in ℝ^{*}$
12	3	sselda	$⊢ (φ \land x \in A) \to x \in [B, C]$
13		iccleub	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in [B, C]) \to x \leq C$
14	9 11 12 13	syl3anc	$⊢ (φ \land x \in A) \to x \leq C$
15	14	ralrimiva	$⊢ φ \to \forall x \in A x \leq C$
16		brralrspcev	$⊢ (C \in ℝ \land \forall x \in A x \leq C) \to \exists y \in ℝ \forall x \in A x \leq y$
17	2 15 16	syl2anc	$⊢ φ \to \exists y \in ℝ \forall x \in A x \leq y$
18		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y) \to sup (A ℝ <) \in ℝ$
19	7 4 17 18	syl3anc	$⊢ φ \to sup (A ℝ <) \in ℝ$
20	7	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
21	3	adantr	$⊢ (φ \land x \in A) \to A \subseteq [B, C]$
22		simpr	$⊢ (φ \land x \in A) \to x \in A$
23		iccsupr	$⊢ ((B \in ℝ \land C \in ℝ) \land A \subseteq [B, C] \land x \in A) \to (A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y)$
24	8 10 21 22 23	syl211anc	$⊢ (φ \land x \in A) \to (A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y)$
25	24 18	syl	$⊢ (φ \land x \in A) \to sup (A ℝ <) \in ℝ$
26		iccgelb	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in [B, C]) \to B \leq x$
27	9 11 12 26	syl3anc	$⊢ (φ \land x \in A) \to B \leq x$
28		suprub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y) \land x \in A) \to x \leq sup (A ℝ <)$
29	24 22 28	syl2anc	$⊢ (φ \land x \in A) \to x \leq sup (A ℝ <)$
30	8 20 25 27 29	letrd	$⊢ (φ \land x \in A) \to B \leq sup (A ℝ <)$
31	30	ralrimiva	$⊢ φ \to \forall x \in A B \leq sup (A ℝ <)$
32		r19.3rzv	$⊢ A \neq \emptyset \to (B \leq sup (A ℝ <) \leftrightarrow \forall x \in A B \leq sup (A ℝ <))$
33	4 32	syl	$⊢ φ \to (B \leq sup (A ℝ <) \leftrightarrow \forall x \in A B \leq sup (A ℝ <))$
34	31 33	mpbird	$⊢ φ \to B \leq sup (A ℝ <)$
35		suprleub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists y \in ℝ \forall x \in A x \leq y) \land C \in ℝ) \to (sup (A ℝ <) \leq C \leftrightarrow \forall x \in A x \leq C)$
36	7 4 17 2 35	syl31anc	$⊢ φ \to (sup (A ℝ <) \leq C \leftrightarrow \forall x \in A x \leq C)$
37	15 36	mpbird	$⊢ φ \to sup (A ℝ <) \leq C$
38		elicc2	$⊢ (B \in ℝ \land C \in ℝ) \to (sup (A ℝ <) \in [B, C] \leftrightarrow (sup (A ℝ <) \in ℝ \land B \leq sup (A ℝ <) \land sup (A ℝ <) \leq C))$
39	1 2 38	syl2anc	$⊢ φ \to (sup (A ℝ <) \in [B, C] \leftrightarrow (sup (A ℝ <) \in ℝ \land B \leq sup (A ℝ <) \land sup (A ℝ <) \leq C))$
40	19 34 37 39	mpbir3and	$⊢ φ \to sup (A ℝ <) \in [B, C]$

Metamath Proof Explorer

Theorem supicc

Proof