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