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 36714

Description: Define the lower bound relationship functor. See brlb 36794 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 36690	. 2 class LB𝑅
3	1	ccnv 5649	. . 3 class ^◡𝑅
4	3	cub 36689	. 2 class UB^◡𝑅
5	2, 4	wceq 1569	1 wff LB𝑅 = UB^◡𝑅

Colors of variables: wff setvar class

This definition is used by: brlb 36794