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