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	|- ( ( _I |` A ) e. Fin <-> A e. Fin )

Proof

Step	Hyp	Ref	Expression
1		dmresi	|- dom ( _I |` A ) = A
2		dmfi	|- ( ( _I |` A ) e. Fin -> dom ( _I |` A ) e. Fin )
3	1 2	eqeltrrid	|- ( ( _I |` A ) e. Fin -> A e. Fin )
4		funi	|- Fun _I
5		funfn	|- ( Fun _I <-> _I Fn dom _I )
6	4 5	mpbi	|- _I Fn dom _I
7		resfnfinfin	|- ( ( _I Fn dom _I /\ A e. Fin ) -> ( _I |` A ) e. Fin )
8	6 7	mpan	|- ( A e. Fin -> ( _I |` A ) e. Fin )
9	3 8	impbii	|- ( ( _I |` A ) e. Fin <-> A e. Fin )