Metamath Proof Explorer

Theorem supclt

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

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

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 supcl ⊢ R Or A ∧ ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → sup B A R ∈ A