Definition df-inf 7060

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

This definition is referenced by:  infeq1  7086  infeq2  7089  infeq3  7090  infeq123d  7091  nfinf  7092  eqinfti  7095  infvalti  7097  infclti  7098  inflbti  7099  infglbti  7100  infsnti  7105  inf00  7106  infisoti  7107  infex2g  7109  dfinfre  9000  infrenegsupex  9685  infxrnegsupex  11445