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→ 𝐴