Theorem eqsupd

Description: Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015)

	Ref	Expression
Hypotheses	supmo.1	$$⊢\phi \to R\mathrm{Or}A$$
	eqsupd.2	$$⊢\phi \to C\in A$$
	eqsupd.3	$$⊢\left(\phi \wedge y\in B\right)\to \neg CRy$$
	eqsupd.4	$$⊢\left(\phi \wedge \left(y\in A\wedge yRC\right)\right)\to \exists z\in ByRz$$
Assertion	eqsupd	$$⊢\phi \to sup\left(B,A,R\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		supmo.1	$$⊢\phi \to R\mathrm{Or}A$$
2		eqsupd.2	$$⊢\phi \to C\in A$$
3		eqsupd.3	$$⊢\left(\phi \wedge y\in B\right)\to \neg CRy$$
4		eqsupd.4	$$⊢\left(\phi \wedge \left(y\in A\wedge yRC\right)\right)\to \exists z\in ByRz$$
5	3	ralrimiva	$$⊢\phi \to \forall y\in B\neg CRy$$
6	4	expr	$$⊢\left(\phi \wedge y\in A\right)\to \left(yRC\to \exists z\in ByRz\right)$$
7	6	ralrimiva	$$⊢\phi \to \forall y\in A\left(yRC\to \exists z\in ByRz\right)$$
8	1	eqsup	$$⊢\phi \to \left(\left(C\in A\wedge \forall y\in B\neg CRy\wedge \forall y\in A\left(yRC\to \exists z\in ByRz\right)\right)\to sup\left(B,A,R\right)=C\right)$$
9	2 5 7 8	mp3and	$$⊢\phi \to sup\left(B,A,R\right)=C$$