Metamath Proof Explorer

Theorem supubt

Description: Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion supubt ⊢ R Or A ∧ ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → C ∈ B → ¬ sup B A R R C

Proof

Step Hyp Ref Expression
1 simpl ⊢ R Or A ∧ ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → R Or A
2 simpr ⊢ R Or A ∧ ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
3 1 2 supub ⊢ R Or A ∧ ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → C ∈ B → ¬ sup B A R R C