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	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑣}$$

Proof

Step	Hyp	Ref	Expression
1		df-resv	$$⊢{\upharpoonright }_{𝑣}=\left(y\in \mathrm{V},x\in \mathrm{V}⟼if\left({\mathrm{Base}}_{\mathrm{Scalar}\left(y\right)}\subseteq x,y,y\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(y\right){\upharpoonright }_{𝑠}x⟩\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑣}$$