Metamath Proof Explorer

Theorem iccsupr

Description: A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl ). (Contributed by Paul Chapman, 21-Jan-2008)

		Ref	Expression
	Assertion	iccsupr	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B] \land C \in S) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S y \leq x)$

Proof

Step	Hyp	Ref	Expression
1		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
2		sstr	$⊢ (S \subseteq [A, B] \land [A, B] \subseteq ℝ) \to S \subseteq ℝ$
3	2	ancoms	$⊢ ([A, B] \subseteq ℝ \land S \subseteq [A, B]) \to S \subseteq ℝ$
4	1 3	sylan	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B]) \to S \subseteq ℝ$
5	4	3adant3	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B] \land C \in S) \to S \subseteq ℝ$
6		ne0i	$⊢ C \in S \to S \neq \emptyset$
7	6	3ad2ant3	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B] \land C \in S) \to S \neq \emptyset$
8		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B]) \to B \in ℝ$
9		ssel	$⊢ S \subseteq [A, B] \to (y \in S \to y \in [A, B])$
10		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
11	10	biimpd	$⊢ (A \in ℝ \land B \in ℝ) \to (y \in [A, B] \to (y \in ℝ \land A \leq y \land y \leq B))$
12	9 11	sylan9r	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B]) \to (y \in S \to (y \in ℝ \land A \leq y \land y \leq B))$
13	12	imp	$⊢ (((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B]) \land y \in S) \to (y \in ℝ \land A \leq y \land y \leq B)$
14	13	simp3d	$⊢ (((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B]) \land y \in S) \to y \leq B$
15	14	ralrimiva	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B]) \to \forall y \in S y \leq B$
16		brralrspcev	$⊢ (B \in ℝ \land \forall y \in S y \leq B) \to \exists x \in ℝ \forall y \in S y \leq x$
17	8 15 16	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B]) \to \exists x \in ℝ \forall y \in S y \leq x$
18	17	3adant3	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B] \land C \in S) \to \exists x \in ℝ \forall y \in S y \leq x$
19	5 7 18	3jca	$⊢ ((A \in ℝ \land B \in ℝ) \land S \subseteq [A, B] \land C \in S) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists x \in ℝ \forall y \in S y \leq x)$