Definition df-ub 33915

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

Assertion

Ref	Expression
df-ub	⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E ))

Detailed syntax breakdown of Definition df-ub

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	cub 33891	. 2 class UB𝑅
3		cvv 3408	. . . 4 class V
4	3, 3	cxp 5549	. . 3 class (V × V)
5	3, 1	cdif 3863	. . . 4 class (V ∖ 𝑅)
6		cep 5459	. . . . 5 class E
7	6	ccnv 5550	. . . 4 class ◡ E
8	5, 7	ccom 5555	. . 3 class ((V ∖ 𝑅) ∘ ◡ E )
9	4, 8	cdif 3863	. 2 class ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E ))
10	2, 9	wceq 1543	1 wff UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E ))

This definition is referenced by:  brub  33993