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

Metamath Proof Explorer

Theorem f1ococnv1

Description: The composition of a one-to-one onto function's converse and itself equals the identity relation restricted to the function's domain. (Contributed by NM, 13-Dec-2003)

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

Proof

Step Hyp Ref Expression
1 f1orel ⊢ F : A ⟶ 1-1 onto B → Rel ⁡ F
2 dfrel2 ⊢ Rel ⁡ F ↔ F -1 -1 = F
3 1 2 sylib ⊢ F : A ⟶ 1-1 onto B → F -1 -1 = F
4 3 coeq2d ⊢ F : A ⟶ 1-1 onto B → F -1 ∘ F -1 -1 = F -1 ∘ F
5 f1ocnv ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A
6 f1ococnv2 ⊢ F -1 : B ⟶ 1-1 onto A → F -1 ∘ F -1 -1 = I ↾ A
7 5 6 syl ⊢ F : A ⟶ 1-1 onto B → F -1 ∘ F -1 -1 = I ↾ A
8 4 7 eqtr3d ⊢ F : A ⟶ 1-1 onto B → F -1 ∘ F = I ↾ A