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