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\leftrightarrow {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$$