Theorem residfi

Description: A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020)

	Ref	Expression
Assertion	residfi	$$⊢{\mathrm{I}\upharpoonright }_A\in \mathrm{Fin}\leftrightarrow A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		dmresi	$$⊢\mathrm{dom}\left({\mathrm{I}\upharpoonright }_A\right)=A$$
2		dmfi	$$⊢{\mathrm{I}\upharpoonright }_A\in \mathrm{Fin}\to \mathrm{dom}\left({\mathrm{I}\upharpoonright }_A\right)\in \mathrm{Fin}$$
3	1 2	eqeltrrid	$$⊢{\mathrm{I}\upharpoonright }_A\in \mathrm{Fin}\to A\in \mathrm{Fin}$$
4		funi	$$⊢\mathrm{Fun}\mathrm{I}$$
5		funfn	$$⊢\mathrm{Fun}\mathrm{I}\leftrightarrow \mathrm{I}Fn\mathrm{dom}\mathrm{I}$$
6	4 5	mpbi	$$⊢\mathrm{I}Fn\mathrm{dom}\mathrm{I}$$
7		resfnfinfin	$$⊢\left(\mathrm{I}Fn\mathrm{dom}\mathrm{I}\wedge A\in \mathrm{Fin}\right)\to {\mathrm{I}\upharpoonright }_A\in \mathrm{Fin}$$
8	6 7	mpan	$$⊢A\in \mathrm{Fin}\to {\mathrm{I}\upharpoonright }_A\in \mathrm{Fin}$$
9	3 8	impbii	$$⊢{\mathrm{I}\upharpoonright }_A\in \mathrm{Fin}\leftrightarrow A\in \mathrm{Fin}$$