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 ( 𝐵 , ∅ , 𝑅 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-inf	⊢ inf ( 𝐵 , ∅ , 𝑅 ) = sup ( 𝐵 , ∅ , ◡ 𝑅 )
2		sup00	⊢ sup ( 𝐵 , ∅ , ◡ 𝑅 ) = ∅
3	1 2	eqtri	⊢ inf ( 𝐵 , ∅ , 𝑅 ) = ∅