Description: The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | sup00 | |- sup ( B , (/) , R ) = (/) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sup | |- sup ( B , (/) , R ) = U. { x e. (/) | ( A. y e. B -. x R y /\ A. y e. (/) ( y R x -> E. z e. B y R z ) ) } |
|
2 | rab0 | |- { x e. (/) | ( A. y e. B -. x R y /\ A. y e. (/) ( y R x -> E. z e. B y R z ) ) } = (/) |
|
3 | 2 | unieqi | |- U. { x e. (/) | ( A. y e. B -. x R y /\ A. y e. (/) ( y R x -> E. z e. B y R z ) ) } = U. (/) |
4 | uni0 | |- U. (/) = (/) |
|
5 | 1 3 4 | 3eqtri | |- sup ( B , (/) , R ) = (/) |