Theorem supex2g

Description: Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	supex2g	|- ( A e. C -> sup ( B , A , R ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		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 ) ) }
2		rabexg	|- ( A e. C -> { 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 )
3	2	uniexd	|- ( A e. C -> 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 )
4	1 3	eqeltrid	|- ( A e. C -> sup ( B , A , R ) e. _V )