Definition df-inf 6398

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 6396	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 4362	. . 3 class ◡𝑅
6	1, 2, 5	csup 6395	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1284	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  6424  infeq2  6427  infeq3  6428  infeq123d  6429  nfinf  6430  eqinfti  6433  infvalti  6435  infclti  6436  inflbti  6437  infglbti  6438  infsnti  6443  inf00  6444  infisoti  6445  dfinfre  8034  infrenegsupex  8682