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 φ C Cat
invid.x φ X B
Assertion invid φ 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 φ C Cat
4 invid.x φ X B
5 1 2 3 4 sectid φ 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 φ 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 φ I X X Inv C X I X