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
|- ( ph -> R Or A )
Assertion supexd
|- ( ph -> sup ( B , A , R ) e. _V )

Proof

Step Hyp Ref Expression
1 supmo.1
 |-  ( ph -> R Or A )
2 df-sup
 |-  sup ( B , A , R ) = U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) }
3 1 supmo
 |-  ( ph -> E* x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
4 rmorabex
 |-  ( E* x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } e. _V )
5 uniexg
 |-  ( { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } e. _V -> U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } e. _V )
6 3 4 5 3syl
 |-  ( ph -> U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } e. _V )
7 2 6 eqeltrid
 |-  ( ph -> sup ( B , A , R ) e. _V )