sn-suprubd

	Ref	Expression
Hypotheses	sn-sup3d.1	$⊢ φ \to A \subseteq ℝ$
	sn-sup3d.2	$⊢ φ \to A \neq \emptyset$
	sn-sup3d.3	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
	sn-suprubd.4	$⊢ φ \to B \in A$
Assertion	sn-suprubd	$⊢ φ \to B \leq sup (A ℝ <)$

Step	Hyp	Ref	Expression
1		sn-sup3d.1	$⊢ φ \to A \subseteq ℝ$
2		sn-sup3d.2	$⊢ φ \to A \neq \emptyset$
3		sn-sup3d.3	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
4		sn-suprubd.4	$⊢ φ \to B \in A$
5	1 4	sseldd	$⊢ φ \to B \in ℝ$
6	1 2 3	sn-suprcld	$⊢ φ \to sup (A ℝ <) \in ℝ$
7		ltso	$⊢ < Or ℝ$
8	7	a1i	$⊢ φ \to < Or ℝ$
9	1 2 3	sn-sup3d	$⊢ φ \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$
10	8 9	supub	$⊢ φ \to (B \in A \to \neg sup (A ℝ <) < B)$
11	4 10	mpd	$⊢ φ \to \neg sup (A ℝ <) < B$
12	5 6 11	nltled	$⊢ φ \to B \leq sup (A ℝ <)$

Metamath Proof Explorer