Definition df-inf 9401

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 9399	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 5640	. . 3 class ◡𝑅
6	1, 2, 5	csup 9398	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1540	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  9435  infeq2  9438  infeq3  9439  infeq123d  9440  nfinf  9441  infexd  9442  eqinf  9443  infval  9445  infcl  9447  inflb  9448  infglb  9449  infglbb  9450  fiinfcl  9461  infltoreq  9462  inf00  9466  infempty  9467  infiso  9468  dfinfre  12171  infrenegsup  12173  tosglb  32908  rencldnfilem  42815