Metamath Proof Explorer


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