Metamath Proof Explorer

Theorem supnub

Description: An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004)

Ref Expression
Hypotheses supmo.1 ⊢ φ → R Or A
supcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
Assertion supnub ⊢ φ → C ∈ A ∧ ∀ z ∈ B ¬ C R z → ¬ C R sup B A R

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢ φ → R Or A
2 supcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
3 1 2 suplub ⊢ φ → C ∈ A ∧ C R sup B A R → ∃ z ∈ B C R z
4 3 expdimp ⊢ φ ∧ C ∈ A → C R sup B A R → ∃ z ∈ B C R z
5 dfrex2 ⊢ ∃ z ∈ B C R z ↔ ¬ ∀ z ∈ B ¬ C R z
6 4 5 syl6ib ⊢ φ ∧ C ∈ A → C R sup B A R → ¬ ∀ z ∈ B ¬ C R z
7 6 con2d ⊢ φ ∧ C ∈ A → ∀ z ∈ B ¬ C R z → ¬ C R sup B A R
8 7 expimpd ⊢ φ → C ∈ A ∧ ∀ z ∈ B ¬ C R z → ¬ C R sup B A R