Metamath Proof Explorer

Theorem f1oiOLD

Description: Obsolete version of f1oi as of 10-Feb-2026. (Contributed by NM, 30-Apr-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion f1oiOLD ⊢ 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