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 X. _V ) \ ( ( _V \ R ) o. `' _E ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 0 cub 
 |-  UB R
2 cvv 
 |-  _V
3 2 2 cxp 
 |-  ( _V X. _V )
4 2 0 cdif 
 |-  ( _V \ R )
5 cep 
 |-  _E
6 5 ccnv 
 |-  `' _E
7 4 6 ccom 
 |-  ( ( _V \ R ) o. `' _E )
8 3 7 cdif 
 |-  ( ( _V X. _V ) \ ( ( _V \ R ) o. `' _E ) )
9 1 8 wceq 
 |-  UB R = ( ( _V X. _V ) \ ( ( _V \ R ) o. `' _E ) )