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