Definition df-sup 8348

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 13977. See dfsup2 8350 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.)

Assertion

Ref	Expression
df-sup	|- sup ( A , B , R ) = U. { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) }

Distinct variable groups:   x, y, z, R   x, A, y, z   x, B, y, z

Detailed syntax breakdown of Definition df-sup

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cR	. . 3 class R
4	1, 2, 3	csup 8346	. 2 class sup ( A , B , R )
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1482	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1482	. . . . . . . 8 class y
9	6, 8, 3	wbr 4653	. . . . . . 7 wff x R y
10	9	wn 3	. . . . . 6 wff -. x R y
11	10, 7, 1	wral 2912	. . . . 5 wff A. y e. A -. x R y
12	8, 6, 3	wbr 4653	. . . . . . 7 wff y R x
13		vz	. . . . . . . . . 10 setvar z
14	13	cv 1482	. . . . . . . . 9 class z
15	8, 14, 3	wbr 4653	. . . . . . . 8 wff y R z
16	15, 13, 1	wrex 2913	. . . . . . 7 wff E. z e. A y R z
17	12, 16	wi 4	. . . . . 6 wff ( y R x -> E. z e. A y R z )
18	17, 7, 2	wral 2912	. . . . 5 wff A. y e. B ( y R x -> E. z e. A y R z )
19	11, 18	wa 384	. . . 4 wff ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) )
20	19, 5, 2	crab 2916	. . 3 class { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) }
21	20	cuni 4436	. 2 class U. { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) }
22	4, 21	wceq 1483	1 wff sup ( A , B , R ) = U. { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) }

This definition is referenced by:  dfsup2  8350  supeq1  8351  supeq2  8354  supeq3  8355  supeq123d  8356  supexd  8359  supval2  8361  sup00  8370  dfinfre  11004  prdsds  16124  supex2g  33532