Metamath Proof Explorer


Definition df-inf

Description: Define the infimum of class A . It is meaningful when R is a relation that strictly orders B and when the infimum exists. For example, R could be 'less than', B could be the set of real numbers, and A could be the set of all positive reals; in this case the infimum is 0. The infimum is defined as the supremum using the converse ordering relation. In the given example, 0 is the supremum of all reals (greatest real number) for which all positive reals are greater. (Contributed by AV, 2-Sep-2020)

Ref Expression
Assertion df-inf
|- inf ( A , B , R ) = sup ( A , B , `' R )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cB
 |-  B
2 cR
 |-  R
3 0 1 2 cinf
 |-  inf ( A , B , R )
4 2 ccnv
 |-  `' R
5 0 1 4 csup
 |-  sup ( A , B , `' R )
6 3 5 wceq
 |-  inf ( A , B , R ) = sup ( A , B , `' R )