Metamath Proof Explorer


Theorem supmax

Description: The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008) (Proof shortened by OpenAI, 30-Mar-2020)

Ref Expression
Hypotheses supmax.1
|- ( ph -> R Or A )
supmax.2
|- ( ph -> C e. A )
supmax.3
|- ( ph -> C e. B )
supmax.4
|- ( ( ph /\ y e. B ) -> -. C R y )
Assertion supmax
|- ( ph -> sup ( B , A , R ) = C )

Proof

Step Hyp Ref Expression
1 supmax.1
 |-  ( ph -> R Or A )
2 supmax.2
 |-  ( ph -> C e. A )
3 supmax.3
 |-  ( ph -> C e. B )
4 supmax.4
 |-  ( ( ph /\ y e. B ) -> -. C R y )
5 simprr
 |-  ( ( ph /\ ( y e. A /\ y R C ) ) -> y R C )
6 breq2
 |-  ( z = C -> ( y R z <-> y R C ) )
7 6 rspcev
 |-  ( ( C e. B /\ y R C ) -> E. z e. B y R z )
8 3 5 7 syl2an2r
 |-  ( ( ph /\ ( y e. A /\ y R C ) ) -> E. z e. B y R z )
9 1 2 4 8 eqsupd
 |-  ( ph -> sup ( B , A , R ) = C )