Metamath Proof Explorer

Theorem supubt

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

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

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	supub	\|- ( ( 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 ) ) ) -> ( C e. B -> -. sup ( B , A , R ) R C ) )

Step

Hyp

Ref

Expression

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 )

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 ) ) )

1 2

supub

 |-  ( ( 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 ) ) ) -> ( C e. B -> -. sup ( B , A , R ) R C ) )