Theorem inf00

Description: The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020)

	Ref	Expression
Assertion	inf00	$$⊢inf\left(B,\varnothing ,R\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-inf	$$⊢inf\left(B,\varnothing ,R\right)=sup\left(B,\varnothing ,R^{-1}\right)$$
2		sup00	$$⊢sup\left(B,\varnothing ,R^{-1}\right)=\varnothing$$
3	1 2	eqtri	$$⊢inf\left(B,\varnothing ,R\right)=\varnothing$$