Theorem suprlubrd

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

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

Proof

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