01sqrexlem3

	Ref	Expression
Hypotheses	01sqrexlem1.1	$⊢ S = \{x \in ℝ^{+} \| x^{2} \leq A\}$
	01sqrexlem1.2	$⊢ B = sup (S ℝ <)$
Assertion	01sqrexlem3	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists z \in ℝ \forall y \in S y \leq z)$

Step	Hyp	Ref	Expression
1		01sqrexlem1.1	$⊢ S = \{x \in ℝ^{+} \| x^{2} \leq A\}$
2		01sqrexlem1.2	$⊢ B = sup (S ℝ <)$
3		ssrab2	$⊢ \{x \in ℝ^{+} \| x^{2} \leq A\} \subseteq ℝ^{+}$
4		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
5	3 4	sstri	$⊢ \{x \in ℝ^{+} \| x^{2} \leq A\} \subseteq ℝ$
6	1 5	eqsstri	$⊢ S \subseteq ℝ$
7	6	a1i	$⊢ (A \in ℝ^{+} \land A \leq 1) \to S \subseteq ℝ$
8	1 2	01sqrexlem2	$⊢ (A \in ℝ^{+} \land A \leq 1) \to A \in S$
9	8	ne0d	$⊢ (A \in ℝ^{+} \land A \leq 1) \to S \neq \emptyset$
10		1re	$⊢ 1 \in ℝ$
11	1 2	01sqrexlem1	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \forall y \in S y \leq 1$
12		brralrspcev	$⊢ (1 \in ℝ \land \forall y \in S y \leq 1) \to \exists z \in ℝ \forall y \in S y \leq z$
13	10 11 12	sylancr	$⊢ (A \in ℝ^{+} \land A \leq 1) \to \exists z \in ℝ \forall y \in S y \leq z$
14	7 9 13	3jca	$⊢ (A \in ℝ^{+} \land A \leq 1) \to (S \subseteq ℝ \land S \neq \emptyset \land \exists z \in ℝ \forall y \in S y \leq z)$

Metamath Proof Explorer