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 ( 𝜑𝑅 Or 𝐴 )
supmax.2 ( 𝜑𝐶𝐴 )
supmax.3 ( 𝜑𝐶𝐵 )
supmax.4 ( ( 𝜑𝑦𝐵 ) → ¬ 𝐶 𝑅 𝑦 )
Assertion supmax ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 supmax.1 ( 𝜑𝑅 Or 𝐴 )
2 supmax.2 ( 𝜑𝐶𝐴 )
3 supmax.3 ( 𝜑𝐶𝐵 )
4 supmax.4 ( ( 𝜑𝑦𝐵 ) → ¬ 𝐶 𝑅 𝑦 )
5 simprr ( ( 𝜑 ∧ ( 𝑦𝐴𝑦 𝑅 𝐶 ) ) → 𝑦 𝑅 𝐶 )
6 breq2 ( 𝑧 = 𝐶 → ( 𝑦 𝑅 𝑧𝑦 𝑅 𝐶 ) )
7 6 rspcev ( ( 𝐶𝐵𝑦 𝑅 𝐶 ) → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 )
8 3 5 7 syl2an2r ( ( 𝜑 ∧ ( 𝑦𝐴𝑦 𝑅 𝐶 ) ) → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 )
9 1 2 4 8 eqsupd ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 )