Definition df-inf 8349

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 8347	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 5113	. . 3 class ◡𝑅
6	1, 2, 5	csup 8346	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1483	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  8382  infeq2  8385  infeq3  8386  infeq123d  8387  nfinf  8388  infexd  8389  eqinf  8390  infval  8392  infcl  8394  inflb  8395  infglb  8396  infglbb  8397  fiinfcl  8407  infltoreq  8408  inf00  8411  infempty  8412  infiso  8413  dfinfre  11004  infrenegsup  11006  tosglb  29670  rencldnfilem  37384