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