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 ( 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 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2		cR	|- R
3	0 1 2	csup	|- sup ( A , B , R )
4		vx	|- x
5		vy	|- y
6	4	cv	|- x
7	5	cv	|- y
8	6 7 2	wbr	|- x R y
9	8	wn	|- -. x R y
10	9 5 0	wral	|- A. y e. A -. x R y
11	7 6 2	wbr	|- y R x
12		vz	|- z
13	12	cv	|- z
14	7 13 2	wbr	|- y R z
15	14 12 0	wrex	|- E. z e. A y R z
16	11 15	wi	|- ( y R x -> E. z e. A y R z )
17	16 5 1	wral	|- A. y e. B ( y R x -> E. z e. A y R z )
18	10 17	wa	|- ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) )
19	18 4 1	crab	|- { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) }
20	19	cuni	|- 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 ) ) }
21	3 20	wceq	|- 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 ) ) }