Metamath Proof Explorer


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 ( 𝐴 , ℝ , < ) ∈ ℝ )