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

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 )