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 ↾ A : A ⟶ 1-1 onto A

Proof

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