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