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 ↾ 𝐴 ) : 𝐴1-1-onto𝐴

Proof

Step Hyp Ref Expression
1 fnresi ( I ↾ 𝐴 ) Fn 𝐴
2 cnvresid ( I ↾ 𝐴 ) = ( I ↾ 𝐴 )
3 2 fneq1i ( ( I ↾ 𝐴 ) Fn 𝐴 ↔ ( I ↾ 𝐴 ) Fn 𝐴 )
4 1 3 mpbir ( I ↾ 𝐴 ) Fn 𝐴
5 dff1o4 ( ( I ↾ 𝐴 ) : 𝐴1-1-onto𝐴 ↔ ( ( I ↾ 𝐴 ) Fn 𝐴 ( I ↾ 𝐴 ) Fn 𝐴 ) )
6 1 4 5 mpbir2an ( I ↾ 𝐴 ) : 𝐴1-1-onto𝐴