Theorem resdmres

Description: Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007)

	Ref	Expression
Assertion	resdmres	$$⊢{A\upharpoonright }_{\mathrm{dom}\left({A\upharpoonright }_B\right)}={A\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		in12	$$⊢A\cap \left(\left(B\times \mathrm{V}\right)\cap \left(\mathrm{dom}A\times \mathrm{V}\right)\right)=\left(B\times \mathrm{V}\right)\cap \left(A\cap \left(\mathrm{dom}A\times \mathrm{V}\right)\right)$$
2		df-res	$$⊢{A\upharpoonright }_{\mathrm{dom}A}=A\cap \left(\mathrm{dom}A\times \mathrm{V}\right)$$
3		resdm2	$$⊢{A\upharpoonright }_{\mathrm{dom}A}={A^{-1}}^{-1}$$
4	2 3	eqtr3i	$$⊢A\cap \left(\mathrm{dom}A\times \mathrm{V}\right)={A^{-1}}^{-1}$$
5	4	ineq2i	$$⊢\left(B\times \mathrm{V}\right)\cap \left(A\cap \left(\mathrm{dom}A\times \mathrm{V}\right)\right)=\left(B\times \mathrm{V}\right)\cap {A^{-1}}^{-1}$$
6		incom	$$⊢\left(B\times \mathrm{V}\right)\cap {A^{-1}}^{-1}={A^{-1}}^{-1}\cap \left(B\times \mathrm{V}\right)$$
7	1 5 6	3eqtri	$$⊢A\cap \left(\left(B\times \mathrm{V}\right)\cap \left(\mathrm{dom}A\times \mathrm{V}\right)\right)={A^{-1}}^{-1}\cap \left(B\times \mathrm{V}\right)$$
8		df-res	$$⊢{A\upharpoonright }_{\mathrm{dom}\left({A\upharpoonright }_B\right)}=A\cap \left(\mathrm{dom}\left({A\upharpoonright }_B\right)\times \mathrm{V}\right)$$
9		dmres	$$⊢\mathrm{dom}\left({A\upharpoonright }_B\right)=B\cap \mathrm{dom}A$$
10	9	xpeq1i	$$⊢\mathrm{dom}\left({A\upharpoonright }_B\right)\times \mathrm{V}=\left(B\cap \mathrm{dom}A\right)\times \mathrm{V}$$
11		xpindir	$$⊢\left(B\cap \mathrm{dom}A\right)\times \mathrm{V}=\left(B\times \mathrm{V}\right)\cap \left(\mathrm{dom}A\times \mathrm{V}\right)$$
12	10 11	eqtri	$$⊢\mathrm{dom}\left({A\upharpoonright }_B\right)\times \mathrm{V}=\left(B\times \mathrm{V}\right)\cap \left(\mathrm{dom}A\times \mathrm{V}\right)$$
13	12	ineq2i	$$⊢A\cap \left(\mathrm{dom}\left({A\upharpoonright }_B\right)\times \mathrm{V}\right)=A\cap \left(\left(B\times \mathrm{V}\right)\cap \left(\mathrm{dom}A\times \mathrm{V}\right)\right)$$
14	8 13	eqtri	$$⊢{A\upharpoonright }_{\mathrm{dom}\left({A\upharpoonright }_B\right)}=A\cap \left(\left(B\times \mathrm{V}\right)\cap \left(\mathrm{dom}A\times \mathrm{V}\right)\right)$$
15		df-res	$$⊢{{A^{-1}}^{-1}\upharpoonright }_B={A^{-1}}^{-1}\cap \left(B\times \mathrm{V}\right)$$
16	7 14 15	3eqtr4i	$$⊢{A\upharpoonright }_{\mathrm{dom}\left({A\upharpoonright }_B\right)}={{A^{-1}}^{-1}\upharpoonright }_B$$
17		rescnvcnv	$$⊢{{A^{-1}}^{-1}\upharpoonright }_B={A\upharpoonright }_B$$
18	16 17	eqtri	$$⊢{A\upharpoonright }_{\mathrm{dom}\left({A\upharpoonright }_B\right)}={A\upharpoonright }_B$$