Definition df-inf 6824

Description: Define the infimum of class A. It is meaningful when R is a relation that strictly orders B and when the infimum exists. For example, R could be 'less than', B could be the set of real numbers, and A 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 ( A , B , R ) = sup ( A , B , `' R )

Detailed syntax breakdown of Definition df-inf

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cR	. . 3 class R
4	1, 2, 3	cinf 6822	. 2 class inf ( A , B , R )
5	3	ccnv 4498	. . 3 class `' R
6	1, 2, 5	csup 6821	. 2 class sup ( A , B , `' R )
7	4, 6	wceq 1314	1 wff inf ( A , B , R ) = sup ( A , B , `' R )

This definition is referenced by:  infeq1  6850  infeq2  6853  infeq3  6854  infeq123d  6855  nfinf  6856  eqinfti  6859  infvalti  6861  infclti  6862  inflbti  6863  infglbti  6864  infsnti  6869  inf00  6870  infisoti  6871  dfinfre  8624  infrenegsupex  9291  infxrnegsupex  10924