Metamath Proof Explorer


Theorem invid

Description: The inverse of the identity is the identity. (Contributed by AV, 8-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 invid
|- ( ph -> ( I ` X ) ( X ( Inv ` C ) 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 1 2 3 4 sectid
 |-  ( ph -> ( I ` X ) ( X ( Sect ` C ) X ) ( I ` X ) )
6 eqid
 |-  ( Inv ` C ) = ( Inv ` C )
7 eqid
 |-  ( Sect ` C ) = ( Sect ` C )
8 1 6 3 4 4 7 isinv
 |-  ( ph -> ( ( I ` X ) ( X ( Inv ` C ) X ) ( I ` X ) <-> ( ( I ` X ) ( X ( Sect ` C ) X ) ( I ` X ) /\ ( I ` X ) ( X ( Sect ` C ) X ) ( I ` X ) ) ) )
9 5 5 8 mpbir2and
 |-  ( ph -> ( I ` X ) ( X ( Inv ` C ) X ) ( I ` X ) )