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

Metamath Proof Explorer

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 )