Theorem suprleubrd

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

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

Proof

Step	Hyp	Ref	Expression
1		suprleubrd.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		suprleubrd.2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		suprleubrd.3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4		suprleubrd.4	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		suprleubrd.5	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝐵 )
6		suprleub	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( sup ( 𝐴 , ℝ , < ) ≤ 𝐵 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝐵 ) )
7	1 2 3 4 6	syl31anc	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) ≤ 𝐵 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝐵 ) )
8	7	bicomd	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝐵 ↔ sup ( 𝐴 , ℝ , < ) ≤ 𝐵 ) )
9	8	biimpd	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝐵 → sup ( 𝐴 , ℝ , < ) ≤ 𝐵 ) )
10	9	imp	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝐵 ) → sup ( 𝐴 , ℝ , < ) ≤ 𝐵 )
11	5 10	mpdan	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ≤ 𝐵 )