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

Proof

Step	Hyp	Ref	Expression
1		df-ress	$$⊢{\upharpoonright }_{𝑠}=\left(w\in \mathrm{V},a\in \mathrm{V}⟼if\left({\mathrm{Base}}_w\subseteq a,w,w\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},a\cap {\mathrm{Base}}_w⟩\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$