Definition df-sup

Description: Define the supremum of class A . It is meaningful when R is a relation that strictly orders B and when the supremum exists. For example, R could be 'less than', B could be the set of real numbers, and A could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrtval . See dfsup2 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999)

	Ref	Expression
Assertion	df-sup	$$⊢sup\left(A,B,R\right)=\bigcup \left\{x\in B|\left(\forall y\in A\neg xRy\wedge \forall y\in B\left(yRx\to \exists z\in AyRz\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		cR	$$classR$$
3	0 1 2	csup	$$classsup\left(A,B,R\right)$$
4		vx	$$setvarx$$
5		vy	$$setvary$$
6	4	cv	$$setvarx$$
7	5	cv	$$setvary$$
8	6 7 2	wbr	$$wffxRy$$
9	8	wn	$$wff\neg xRy$$
10	9 5 0	wral	$$wff\forall y\in A\neg xRy$$
11	7 6 2	wbr	$$wffyRx$$
12		vz	$$setvarz$$
13	12	cv	$$setvarz$$
14	7 13 2	wbr	$$wffyRz$$
15	14 12 0	wrex	$$wff\exists z\in AyRz$$
16	11 15	wi	$$wff\left(yRx\to \exists z\in AyRz\right)$$
17	16 5 1	wral	$$wff\forall y\in B\left(yRx\to \exists z\in AyRz\right)$$
18	10 17	wa	$$wff\left(\forall y\in A\neg xRy\wedge \forall y\in B\left(yRx\to \exists z\in AyRz\right)\right)$$
19	18 4 1	crab	$$class\left\{x\in B|\left(\forall y\in A\neg xRy\wedge \forall y\in B\left(yRx\to \exists z\in AyRz\right)\right)\right\}$$
20	19	cuni	$$class\bigcup \left\{x\in B|\left(\forall y\in A\neg xRy\wedge \forall y\in B\left(yRx\to \exists z\in AyRz\right)\right)\right\}$$
21	3 20	wceq	$$wffsup\left(A,B,R\right)=\bigcup \left\{x\in B|\left(\forall y\in A\neg xRy\wedge \forall y\in B\left(yRx\to \exists z\in AyRz\right)\right)\right\}$$