Metamath Proof Explorer


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 )