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 )