This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suprcld

Description: Natural deduction form of suprcl . (Contributed by Stanislas Polu, 9-Mar-2020)

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

Step	Hyp	Ref	Expression
1		suprcld.2	$⊢ φ \to A \subseteq ℝ$
2		suprcld.1	$⊢ φ \to A \neq \emptyset$
3		suprcld.4	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
4		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
5	1 2 3 4	syl3anc	$⊢ φ \to sup (A ℝ <) \in ℝ$