Metamath Proof Explorer

Theorem f1oi

Description: A restriction of the identity relation is a one-to-one onto function. (Contributed by NM, 30-Apr-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion f1oi ⊢ I ↾ A : A ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 fnresi ⊢ I ↾ A Fn A
2 cnvresid ⊢ I ↾ A -1 = I ↾ A
3 2 fneq1i ⊢ I ↾ A -1 Fn A ↔ I ↾ A Fn A
4 1 3 mpbir ⊢ I ↾ A -1 Fn A
5 dff1o4 ⊢ I ↾ A : A ⟶ 1-1 onto A ↔ I ↾ A Fn A ∧ I ↾ A -1 Fn A
6 1 4 5 mpbir2an ⊢ I ↾ A : A ⟶ 1-1 onto A