Definition df-inf 8891

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 8889	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 5518	. . 3 class ◡𝑅
6	1, 2, 5	csup 8888	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1538	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  8924  infeq2  8927  infeq3  8928  infeq123d  8929  nfinf  8930  infexd  8931  eqinf  8932  infval  8934  infcl  8936  inflb  8937  infglb  8938  infglbb  8939  fiinfcl  8949  infltoreq  8950  inf00  8954  infempty  8955  infiso  8956  dfinfre  11609  infrenegsup  11611  tosglb  30683  rencldnfilem  39761