Theorem cnvrescnv

Description: Two ways to express the corestriction of a class. (Contributed by BJ, 28-Dec-2023)

	Ref	Expression
Assertion	cnvrescnv	$$⊢{\left({R^{-1}\upharpoonright }_B\right)}^{-1}=R\cap \left(\mathrm{V}\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-res	$$⊢{R^{-1}\upharpoonright }_B=R^{-1}\cap \left(B\times \mathrm{V}\right)$$
2	1	cnveqi	$$⊢{\left({R^{-1}\upharpoonright }_B\right)}^{-1}={\left(R^{-1}\cap \left(B\times \mathrm{V}\right)\right)}^{-1}$$
3		cnvin	$$⊢{\left(R^{-1}\cap \left(B\times \mathrm{V}\right)\right)}^{-1}={R^{-1}}^{-1}\cap {\left(B\times \mathrm{V}\right)}^{-1}$$
4		cnvcnv	$$⊢{R^{-1}}^{-1}=R\cap \left(\mathrm{V}\times \mathrm{V}\right)$$
5		cnvxp	$$⊢{\left(B\times \mathrm{V}\right)}^{-1}=\mathrm{V}\times B$$
6	4 5	ineq12i	$$⊢{R^{-1}}^{-1}\cap {\left(B\times \mathrm{V}\right)}^{-1}=\left(R\cap \left(\mathrm{V}\times \mathrm{V}\right)\right)\cap \left(\mathrm{V}\times B\right)$$
7		inass	$$⊢\left(R\cap \left(\mathrm{V}\times \mathrm{V}\right)\right)\cap \left(\mathrm{V}\times B\right)=R\cap \left(\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(\mathrm{V}\times B\right)\right)$$
8		inxp	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(\mathrm{V}\times B\right)=\left(\mathrm{V}\cap \mathrm{V}\right)\times \left(\mathrm{V}\cap B\right)$$
9		inv1	$$⊢\mathrm{V}\cap \mathrm{V}=\mathrm{V}$$
10	9	eqcomi	$$⊢\mathrm{V}=\mathrm{V}\cap \mathrm{V}$$
11		ssv	$$⊢B\subseteq \mathrm{V}$$
12		ssid	$$⊢B\subseteq B$$
13	11 12	ssini	$$⊢B\subseteq \mathrm{V}\cap B$$
14		inss2	$$⊢\mathrm{V}\cap B\subseteq B$$
15	13 14	eqssi	$$⊢B=\mathrm{V}\cap B$$
16	10 15	xpeq12i	$$⊢\mathrm{V}\times B=\left(\mathrm{V}\cap \mathrm{V}\right)\times \left(\mathrm{V}\cap B\right)$$
17	8 16	eqtr4i	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(\mathrm{V}\times B\right)=\mathrm{V}\times B$$
18	17	ineq2i	$$⊢R\cap \left(\left(\mathrm{V}\times \mathrm{V}\right)\cap \left(\mathrm{V}\times B\right)\right)=R\cap \left(\mathrm{V}\times B\right)$$
19	6 7 18	3eqtri	$$⊢{R^{-1}}^{-1}\cap {\left(B\times \mathrm{V}\right)}^{-1}=R\cap \left(\mathrm{V}\times B\right)$$
20	2 3 19	3eqtri	$$⊢{\left({R^{-1}\upharpoonright }_B\right)}^{-1}=R\cap \left(\mathrm{V}\times B\right)$$