df-lb - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-lb		Structured version Visualization version GIF version

Definition df-lb 31984

Description: Define the lower bound relationship functor. See brlb 32062 for value. (Contributed by Scott Fenton, 3-May-2018.)

**Assertion**
Ref	Expression
df-lb	⊢ LB𝑅 = UB^◡𝑅

**Detailed syntax breakdown of Definition df-lb**
Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	clb 31960	. 2 class LB𝑅
3	1	ccnv 5113	. . 3 class ^◡𝑅
4	3	cub 31959	. 2 class UB^◡𝑅
5	2, 4	wceq 1483	1 wff LB𝑅 = UB^◡𝑅

Colors of variables: wff setvar class

This definition is referenced by: brlb 32062