Theorem cnvresid

Description: Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007)

	Ref	Expression
Assertion	cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}={\mathrm{I}\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		cnvi	$$⊢{\mathrm{I}}^{-1}=\mathrm{I}$$
2	1	eqcomi	$$⊢\mathrm{I}={\mathrm{I}}^{-1}$$
3		funi	$$⊢\mathrm{Fun}\mathrm{I}$$
4		funeq	$$⊢\mathrm{I}={\mathrm{I}}^{-1}\to \left(\mathrm{Fun}\mathrm{I}\leftrightarrow \mathrm{Fun}{\mathrm{I}}^{-1}\right)$$
5	3 4	mpbii	$$⊢\mathrm{I}={\mathrm{I}}^{-1}\to \mathrm{Fun}{\mathrm{I}}^{-1}$$
6		funcnvres	$$⊢\mathrm{Fun}{\mathrm{I}}^{-1}\to {\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}={{\mathrm{I}}^{-1}\upharpoonright }_{\mathrm{I}\left[A\right]}$$
7		imai	$$⊢\mathrm{I}\left[A\right]=A$$
8	1 7	reseq12i	$$⊢{{\mathrm{I}}^{-1}\upharpoonright }_{\mathrm{I}\left[A\right]}={\mathrm{I}\upharpoonright }_A$$
9	6 8	syl6eq	$$⊢\mathrm{Fun}{\mathrm{I}}^{-1}\to {\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}={\mathrm{I}\upharpoonright }_A$$
10	2 5 9	mp2b	$$⊢{\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}={\mathrm{I}\upharpoonright }_A$$