Syntax Definition csup 9129

Description: Extend class notation to include supremum of class 𝐴. Here 𝑅 is ordinarily a relation that strictly orders class 𝐵. For example, 𝑅 could be 'less than' and 𝐵 could be the set of real numbers.

Hypotheses

Ref	Expression
cA	class 𝐴
cB	class 𝐵
cR	class 𝑅

Assertion

Ref	Expression
csup	class sup(𝐴, 𝐵, 𝑅)

See definition df-sup 9131 for more information.