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 ↾ 𝐴 ) ∈ Fin ↔ 𝐴 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		dmresi	⊢ dom ( I ↾ 𝐴 ) = 𝐴
2		dmfi	⊢ ( ( I ↾ 𝐴 ) ∈ Fin → dom ( I ↾ 𝐴 ) ∈ Fin )
3	1 2	eqeltrrid	⊢ ( ( I ↾ 𝐴 ) ∈ Fin → 𝐴 ∈ 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 ∧ 𝐴 ∈ Fin ) → ( I ↾ 𝐴 ) ∈ Fin )
8	6 7	mpan	⊢ ( 𝐴 ∈ Fin → ( I ↾ 𝐴 ) ∈ Fin )
9	3 8	impbii	⊢ ( ( I ↾ 𝐴 ) ∈ Fin ↔ 𝐴 ∈ Fin )