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

Metamath Proof Explorer

Definition df-ub

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

		Ref	Expression
	Assertion	df-ub	$⊢ UB R = (V \times V) ∖ ((V ∖ R) \circ E^{-1})$

Step	Hyp	Ref	Expression
0		cR	$class R$
1	0	cub	$class UB R$
2		cvv	$class V$
3	2 2	cxp	$class (V \times V)$
4	2 0	cdif	$class (V ∖ R)$
5		cep	$class E$
6	5	ccnv	$class E^{-1}$
7	4 6	ccom	$class ((V ∖ R) \circ E^{-1})$
8	3 7	cdif	$class ((V \times V) ∖ ((V ∖ R) \circ E^{-1}))$
9	1 8	wceq	$wff UB R = (V \times V) ∖ ((V ∖ R) \circ E^{-1})$