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	$$⊢\phi \to R\mathrm{Or}A$$
	supmax.2	$$⊢\phi \to C\in A$$
	supmax.3	$$⊢\phi \to C\in B$$
	supmax.4	$$⊢\left(\phi \wedge y\in B\right)\to \neg CRy$$
Assertion	supmax	$$⊢\phi \to sup\left(B,A,R\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		supmax.1	$$⊢\phi \to R\mathrm{Or}A$$
2		supmax.2	$$⊢\phi \to C\in A$$
3		supmax.3	$$⊢\phi \to C\in B$$
4		supmax.4	$$⊢\left(\phi \wedge y\in B\right)\to \neg CRy$$
5		simprr	$$⊢\left(\phi \wedge \left(y\in A\wedge yRC\right)\right)\to yRC$$
6		breq2	$$⊢z=C\to \left(yRz\leftrightarrow yRC\right)$$
7	6	rspcev	$$⊢\left(C\in B\wedge yRC\right)\to \exists z\in ByRz$$
8	3 5 7	syl2an2r	$$⊢\left(\phi \wedge \left(y\in A\wedge yRC\right)\right)\to \exists z\in ByRz$$
9	1 2 4 8	eqsupd	$$⊢\phi \to sup\left(B,A,R\right)=C$$