Metamath Proof Explorer


Theorem sup00

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 ) = (/)

Proof

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 ) = (/)