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

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) Avoid ax-12 . (Revised by TM, 10-Feb-2026)

Ref Expression
Assertion f1oi ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴

Proof

Step Hyp Ref Expression
1 fnresi ⊢ ( I ↾ 𝐴 ) Fn 𝐴
2 funi ⊢ Fun I
3 cnvi ⊢ ◡ I = I
4 3 funeqi ⊢ ( Fun ◡ I ↔ Fun I )
5 2 4 mpbir ⊢ Fun ◡ I
6 funres11 ⊢ ( Fun ◡ I → Fun ◡ ( I ↾ 𝐴 ) )
7 5 6 ax-mp ⊢ Fun ◡ ( I ↾ 𝐴 )
8 rnresi ⊢ ran ( I ↾ 𝐴 ) = 𝐴
9 dff1o2 ⊢ ( ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 ↔ ( ( I ↾ 𝐴 ) Fn 𝐴 ∧ Fun ◡ ( I ↾ 𝐴 ) ∧ ran ( I ↾ 𝐴 ) = 𝐴 ) )
10 1 7 8 9 mpbir3an ⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴