Metamath Proof Explorer

Theorem suprleubrd

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

Ref Expression
Hypotheses suprleubrd.1 ⊢ φ → A ⊆ ℝ
suprleubrd.2 ⊢ φ → A ≠ ∅
suprleubrd.3 ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
suprleubrd.4 ⊢ φ → B ∈ ℝ
suprleubrd.5 ⊢ φ → ∀ z ∈ A z ≤ B
Assertion suprleubrd ⊢ φ → sup A ℝ < ≤ B

Proof

Step Hyp Ref Expression
1 suprleubrd.1 ⊢ φ → A ⊆ ℝ
2 suprleubrd.2 ⊢ φ → A ≠ ∅
3 suprleubrd.3 ⊢ φ → ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
4 suprleubrd.4 ⊢ φ → B ∈ ℝ
5 suprleubrd.5 ⊢ φ → ∀ z ∈ A z ≤ B
6 suprleub ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x ∧ B ∈ ℝ → sup A ℝ < ≤ B ↔ ∀ z ∈ A z ≤ B
7 1 2 3 4 6 syl31anc ⊢ φ → sup A ℝ < ≤ B ↔ ∀ z ∈ A z ≤ B
8 7 bicomd ⊢ φ → ∀ z ∈ A z ≤ B ↔ sup A ℝ < ≤ B
9 8 biimpd ⊢ φ → ∀ z ∈ A z ≤ B → sup A ℝ < ≤ B
10 9 imp ⊢ φ ∧ ∀ z ∈ A z ≤ B → sup A ℝ < ≤ B
11 5 10 mpdan ⊢ φ → sup A ℝ < ≤ B