Metamath Proof Explorer

Theorem reldmress

Description: The structure restriction is a proper operator, so it can be used with ovprc1 . (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Assertion reldmress 
|- Rel dom |`s

Proof

Step Hyp Ref Expression
1 df-ress 
 |-  |`s = ( w e. _V , a e. _V |-> if ( ( Base ` w ) C_ a , w , ( w sSet <. ( Base ` ndx ) , ( a i^i ( Base ` w ) ) >. ) ) )
2 1 reldmmpo 
 |-  Rel dom |`s