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

Metamath Proof Explorer

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