Metamath Proof Explorer

Definition df-lb

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

Ref Expression
Assertion df-lb 
|- LB R = UB `' R

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 0 clb 
 |-  LB R
2 0 ccnv 
 |-  `' R
3 2 cub 
 |-  UB `' R
4 1 3 wceq 
 |-  LB R = UB `' R