Metamath Proof Explorer


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