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

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 ⊢ φ → C ∈ Cat
invid.x ⊢ φ → X ∈ B
Assertion idinv ⊢ φ → 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 ⊢ φ → C ∈ Cat
4 invid.x ⊢ φ → X ∈ B
5 eqid ⊢ Inv ⁡ C = Inv ⁡ C
6 1 5 3 4 4 invfun ⊢ φ → Fun ⁡ X Inv ⁡ C X
7 1 2 3 4 invid ⊢ φ → 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 ⊢ φ → X Inv ⁡ C X ⁡ I ⁡ X = I ⁡ X