Theorem relres

Description: A restriction is a relation. Exercise 12 of TakeutiZaring p. 25. (Contributed by NM, 2-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	relres	$$⊢\mathrm{Rel}\left({A\upharpoonright }_B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-res	$$⊢{A\upharpoonright }_B=A\cap \left(B\times \mathrm{V}\right)$$
2		inss2	$$⊢A\cap \left(B\times \mathrm{V}\right)\subseteq B\times \mathrm{V}$$
3	1 2	eqsstri	$$⊢{A\upharpoonright }_B\subseteq B\times \mathrm{V}$$
4		relxp	$$⊢\mathrm{Rel}\left(B\times \mathrm{V}\right)$$
5		relss	$$⊢{A\upharpoonright }_B\subseteq B\times \mathrm{V}\to \left(\mathrm{Rel}\left(B\times \mathrm{V}\right)\to \mathrm{Rel}\left({A\upharpoonright }_B\right)\right)$$
6	3 4 5	mp2	$$⊢\mathrm{Rel}\left({A\upharpoonright }_B\right)$$