This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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^{-1}$

Step	Hyp	Ref	Expression
0		cR	$class R$
1	0	clb	$class LB R$
2	0	ccnv	$class R^{-1}$
3	2	cub	$class UB R^{-1}$
4	1 3	wceq	$wff LB R = UB R^{-1}$