Theorem suprcld

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

	Ref	Expression
Hypotheses	suprcld.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	suprcld.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	suprcld.4	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
Assertion	suprcld	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		suprcld.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		suprcld.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		suprcld.4	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4		suprcl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )