Metamath Proof Explorer

Theorem supclt

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

Ref Expression
Assertion supclt 
|- ( ( R Or A /\ 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 ) ) ) -> sup ( B , A , R ) e. A )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( R Or A /\ 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 ) ) ) -> R Or A )
2 simpr 
 |-  ( ( R Or A /\ 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 ) ) ) -> 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 2 supcl 
 |-  ( ( R Or A /\ 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 ) ) ) -> sup ( B , A , R ) e. A )