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 sup B R =

Proof

Step Hyp Ref Expression
1 df-inf sup B R = sup B R -1
2 sup00 sup B R -1 =
3 1 2 eqtri sup B R =