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

Metamath Proof Explorer

Theorem f1cocnv1

Description: Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011)

Ref Expression
Assertion f1cocnv1 ⊢ F : A ⟶ 1-1 B → F -1 ∘ F = I ↾ A

Proof

Step Hyp Ref Expression
1 f1f1orn ⊢ F : A ⟶ 1-1 B → F : A ⟶ 1-1 onto ran ⁡ F
2 f1ococnv1 ⊢ F : A ⟶ 1-1 onto ran ⁡ F → F -1 ∘ F = I ↾ A
3 1 2 syl ⊢ F : A ⟶ 1-1 B → F -1 ∘ F = I ↾ A