Theorem suprubd

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

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

Proof

Step	Hyp	Ref	Expression
1		suprubd.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		suprubd.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		suprubd.3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4		suprubd.4	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
5		suprub	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )
6	1 2 3 4 5	syl31anc	⊢ ( 𝜑 → 𝐵 ≤ sup ( 𝐴 , ℝ , < ) )