Metamath Proof Explorer

Theorem supexd

Description: A supremum is a set. (Contributed by NM, 22-May-1999) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis supmo.1 ⊢ φ → R Or A
Assertion supexd ⊢ φ → sup B A R ∈ V

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢ φ → R Or A
2 df-sup ⊢ sup B A R = ⋃ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
3 1 supmo ⊢ φ → ∃* x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
4 rmorabex ⊢ ∃* 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 ∈ V
5 uniexg ⊢ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ∈ V → ⋃ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ∈ V
6 3 4 5 3syl ⊢ φ → ⋃ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ∈ V
7 2 6 eqeltrid ⊢ φ → sup B A R ∈ V