This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ Fin ↔ A ∈ Fin

Proof

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