Metamath Proof Explorer

Theorem reldmresv

Description: The scalar restriction is a proper operator, so it can be used with ovprc1 . (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Assertion reldmresv 
|- Rel dom |`v

Proof

Step Hyp Ref Expression
1 df-resv 
 |-  |`v = ( y e. _V , x e. _V |-> if ( ( Base ` ( Scalar ` y ) ) C_ x , y , ( y sSet <. ( Scalar ` ndx ) , ( ( Scalar ` y ) |`s x ) >. ) ) )
2 1 reldmmpo 
 |-  Rel dom |`v