Definition df-inf 6950

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 6948	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 4603	. . 3 class ◡𝑅
6	1, 2, 5	csup 6947	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1343	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  6976  infeq2  6979  infeq3  6980  infeq123d  6981  nfinf  6982  eqinfti  6985  infvalti  6987  infclti  6988  inflbti  6989  infglbti  6990  infsnti  6995  inf00  6996  infisoti  6997  infex2g  6999  dfinfre  8851  infrenegsupex  9532  infxrnegsupex  11204