This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supcl

Description: A supremum belongs to its base class (closure law). See also supub and suplub . (Contributed by NM, 12-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 supcl ⊢ φ → sup B A R ∈ A

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 supval2 ⊢ φ → sup B A R = ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
4 1 2 supeu ⊢ φ → ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
5 riotacl ⊢ ∃! 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 ∈ A
6 4 5 syl ⊢ φ → ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ∈ A
7 3 6 eqeltrd ⊢ φ → sup B A R ∈ A