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 𝑅 = ( ( V × V ) ∖ ( ( V ∖ 𝑅 ) ∘ ◡ E ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	cub	⊢ UB 𝑅
2		cvv	⊢ V
3	2 2	cxp	⊢ ( V × V )
4	2 0	cdif	⊢ ( V ∖ 𝑅 )
5		cep	⊢ E
6	5	ccnv	⊢ ◡ E
7	4 6	ccom	⊢ ( ( V ∖ 𝑅 ) ∘ ◡ E )
8	3 7	cdif	⊢ ( ( V × V ) ∖ ( ( V ∖ 𝑅 ) ∘ ◡ E ) )
9	1 8	wceq	⊢ UB 𝑅 = ( ( V × V ) ∖ ( ( V ∖ 𝑅 ) ∘ ◡ E ) )