Theorem supcl

Description: A supremum belongs to its base class (closure law). See also supub and suplub . (Contributed by NM, 12-Oct-2004)

	Ref	Expression
Hypotheses	supmo.1	$$⊢\phi \to R\mathrm{Or}A$$
	supcl.2	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg xRy\wedge \forall y\in A\left(yRx\to \exists z\in ByRz\right)\right)$$
Assertion	supcl	$$⊢\phi \to sup\left(B,A,R\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		supmo.1	$$⊢\phi \to R\mathrm{Or}A$$
2		supcl.2	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg xRy\wedge \forall y\in A\left(yRx\to \exists z\in ByRz\right)\right)$$
3	1	supval2	$$⊢\phi \to sup\left(B,A,R\right)=\left(\iota x\in A|\left(\forall y\in B\neg xRy\wedge \forall y\in A\left(yRx\to \exists z\in ByRz\right)\right)\right)$$
4	1 2	supeu	$$⊢\phi \to \exists !x\in A\left(\forall y\in B\neg xRy\wedge \forall y\in A\left(yRx\to \exists z\in ByRz\right)\right)$$
5		riotacl	$$⊢\exists !x\in A\left(\forall y\in B\neg xRy\wedge \forall y\in A\left(yRx\to \exists z\in ByRz\right)\right)\to \left(\iota x\in A|\left(\forall y\in B\neg xRy\wedge \forall y\in A\left(yRx\to \exists z\in ByRz\right)\right)\right)\in A$$
6	4 5	syl	$$⊢\phi \to \left(\iota x\in A|\left(\forall y\in B\neg xRy\wedge \forall y\in A\left(yRx\to \exists z\in ByRz\right)\right)\right)\in A$$
7	3 6	eqeltrd	$$⊢\phi \to sup\left(B,A,R\right)\in A$$