Theorem supnub

Description: An upper bound is not less than the supremum. (Contributed by NM, 13-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	supnub	|- ( ph -> ( ( C e. A /\ A. z e. B -. C R z ) -> -. C R sup ( B , A , R ) ) )

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 2	suplub	|- ( ph -> ( ( C e. A /\ C R sup ( B , A , R ) ) -> E. z e. B C R z ) )
4	3	expdimp	|- ( ( ph /\ C e. A ) -> ( C R sup ( B , A , R ) -> E. z e. B C R z ) )
5		dfrex2	|- ( E. z e. B C R z <-> -. A. z e. B -. C R z )
6	4 5	syl6ib	|- ( ( ph /\ C e. A ) -> ( C R sup ( B , A , R ) -> -. A. z e. B -. C R z ) )
7	6	con2d	|- ( ( ph /\ C e. A ) -> ( A. z e. B -. C R z -> -. C R sup ( B , A , R ) ) )
8	7	expimpd	|- ( ph -> ( ( C e. A /\ A. z e. B -. C R z ) -> -. C R sup ( B , A , R ) ) )