Definition df-inf 7023

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 7021	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 4650	. . 3 class ◡𝑅
6	1, 2, 5	csup 7020	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1364	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  7049  infeq2  7052  infeq3  7053  infeq123d  7054  nfinf  7055  eqinfti  7058  infvalti  7060  infclti  7061  inflbti  7062  infglbti  7063  infsnti  7068  inf00  7069  infisoti  7070  infex2g  7072  dfinfre  8954  infrenegsupex  9636  infxrnegsupex  11318