Metamath Proof Explorer


Theorem idinv

Description: The inverse of the identity is the identity. Example 3.13 of Adamek p. 28. (Contributed by AV, 9-Apr-2020)

Ref Expression
Hypotheses invid.b
|- B = ( Base ` C )
invid.i
|- I = ( Id ` C )
invid.c
|- ( ph -> C e. Cat )
invid.x
|- ( ph -> X e. B )
Assertion idinv
|- ( ph -> ( ( X ( Inv ` C ) X ) ` ( I ` X ) ) = ( I ` X ) )

Proof

Step Hyp Ref Expression
1 invid.b
 |-  B = ( Base ` C )
2 invid.i
 |-  I = ( Id ` C )
3 invid.c
 |-  ( ph -> C e. Cat )
4 invid.x
 |-  ( ph -> X e. B )
5 eqid
 |-  ( Inv ` C ) = ( Inv ` C )
6 1 5 3 4 4 invfun
 |-  ( ph -> Fun ( X ( Inv ` C ) X ) )
7 1 2 3 4 invid
 |-  ( ph -> ( I ` X ) ( X ( Inv ` C ) X ) ( I ` X ) )
8 funbrfv
 |-  ( Fun ( X ( Inv ` C ) X ) -> ( ( I ` X ) ( X ( Inv ` C ) X ) ( I ` X ) -> ( ( X ( Inv ` C ) X ) ` ( I ` X ) ) = ( I ` X ) ) )
9 6 7 8 sylc
 |-  ( ph -> ( ( X ( Inv ` C ) X ) ` ( I ` X ) ) = ( I ` X ) )