Definition df-inf 9391

Description: Define the infimum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the infimum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 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.)

Assertion

Ref	Expression
df-inf	⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

Detailed syntax breakdown of Definition df-inf

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cR	. . 3 class 𝑅
4	1, 2, 3	cinf 9389	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 5651	. . 3 class ◡𝑅
6	1, 2, 5	csup 9388	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1563	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  9425  infeq2  9428  infeq3  9429  infeq123d  9430  nfinf  9431  infexd  9432  eqinf  9433  infval  9435  infcl  9437  inflb  9438  infglb  9439  infglbb  9440  fiinfcl  9451  infltoreq  9452  inf00  9456  infempty  9457  infiso  9458  dfinfre  12187  infrenegsup  12189  tosglb  33208  rencldnfilem  43409