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