Definition df-inf 7175

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 7173	. 2 class inf ( A , B , R )
5	3	ccnv 4722	. . 3 class `' R
6	1, 2, 5	csup 7172	. 2 class sup ( A , B , `' R )
7	4, 6	wceq 1395	1 wff inf ( A , B , R ) = sup ( A , B , `' R )

This definition is referenced by:  infeq1  7201  infeq2  7204  infeq3  7205  infeq123d  7206  nfinf  7207  eqinfti  7210  infvalti  7212  infclti  7213  inflbti  7214  infglbti  7215  infsnti  7220  inf00  7221  infisoti  7222  infex2g  7224  dfinfre  9126  infrenegsupex  9818  infxrnegsupex  11814