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

Proof

Step Hyp Ref Expression
1 df-inf 
 |-  inf ( B , (/) , R ) = sup ( B , (/) , `' R )
2 sup00 
 |-  sup ( B , (/) , `' R ) = (/)
3 1 2 eqtri 
 |-  inf ( B , (/) , R ) = (/)