Theorem supcl

Description: A supremum belongs to its base class (closure law). See also supub and suplub . (Contributed by NM, 12-Oct-2004)

	Ref	Expression
Hypotheses	supmo.1	|- ( ph -> R Or A )
	supcl.2	|- ( 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 ) ) )
Assertion	supcl	|- ( ph -> sup ( B , A , R ) e. A )

Proof

Step	Hyp	Ref	Expression
1		supmo.1	|- ( ph -> R Or A )
2		supcl.2	|- ( 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 ) ) )
3	1	supval2	|- ( ph -> sup ( B , A , R ) = ( iota_ 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	1 2	supeu	|- ( 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 ) ) )
5		riotacl	|- ( 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 ) ) -> ( iota_ 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. A )
6	4 5	syl	|- ( ph -> ( iota_ 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. A )
7	3 6	eqeltrd	|- ( ph -> sup ( B , A , R ) e. A )