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	$$⊢\mathrm{UB}R=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \left(\left(\mathrm{V}\setminus R\right)\circ {\mathrm{E}}^{-1}\right)$$

Detailed syntax breakdown

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