# Metamath Proof Explorer

## Theorem coi2

Description: Composition with the identity relation. Part of Theorem 3.7(i) of Monk1 p. 36. (Contributed by NM, 22-Apr-2004)

Ref Expression
Assertion coi2 ${⊢}\mathrm{Rel}{A}\to \mathrm{I}\circ {A}={A}$

### Proof

Step Hyp Ref Expression
1 dfrel2 ${⊢}\mathrm{Rel}{A}↔{{{A}}^{-1}}^{-1}={A}$
2 cnvco ${⊢}{\left({{A}}^{-1}\circ \mathrm{I}\right)}^{-1}={\mathrm{I}}^{-1}\circ {{{A}}^{-1}}^{-1}$
3 relcnv ${⊢}\mathrm{Rel}{{A}}^{-1}$
4 coi1 ${⊢}\mathrm{Rel}{{A}}^{-1}\to {{A}}^{-1}\circ \mathrm{I}={{A}}^{-1}$
5 3 4 ax-mp ${⊢}{{A}}^{-1}\circ \mathrm{I}={{A}}^{-1}$
6 5 cnveqi ${⊢}{\left({{A}}^{-1}\circ \mathrm{I}\right)}^{-1}={{{A}}^{-1}}^{-1}$
7 2 6 eqtr3i ${⊢}{\mathrm{I}}^{-1}\circ {{{A}}^{-1}}^{-1}={{{A}}^{-1}}^{-1}$
8 cnvi ${⊢}{\mathrm{I}}^{-1}=\mathrm{I}$
9 coeq2 ${⊢}{{{A}}^{-1}}^{-1}={A}\to {\mathrm{I}}^{-1}\circ {{{A}}^{-1}}^{-1}={\mathrm{I}}^{-1}\circ {A}$
10 coeq1 ${⊢}{\mathrm{I}}^{-1}=\mathrm{I}\to {\mathrm{I}}^{-1}\circ {A}=\mathrm{I}\circ {A}$
11 9 10 sylan9eq ${⊢}\left({{{A}}^{-1}}^{-1}={A}\wedge {\mathrm{I}}^{-1}=\mathrm{I}\right)\to {\mathrm{I}}^{-1}\circ {{{A}}^{-1}}^{-1}=\mathrm{I}\circ {A}$
12 8 11 mpan2 ${⊢}{{{A}}^{-1}}^{-1}={A}\to {\mathrm{I}}^{-1}\circ {{{A}}^{-1}}^{-1}=\mathrm{I}\circ {A}$
13 id ${⊢}{{{A}}^{-1}}^{-1}={A}\to {{{A}}^{-1}}^{-1}={A}$
14 7 12 13 3eqtr3a ${⊢}{{{A}}^{-1}}^{-1}={A}\to \mathrm{I}\circ {A}={A}$
15 1 14 sylbi ${⊢}\mathrm{Rel}{A}\to \mathrm{I}\circ {A}={A}$