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