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={\mathrm{Base}}_C$$
	invid.i	$$⊢I=\mathrm{Id}\left(C\right)$$
	invid.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	invid.x	$$⊢\phi \to X\in B$$
Assertion	idinv	$$⊢\phi \to \left(X\mathrm{Inv}\left(C\right)X\right)\left(I\left(X\right)\right)=I\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		invid.b	$$⊢B={\mathrm{Base}}_C$$
2		invid.i	$$⊢I=\mathrm{Id}\left(C\right)$$
3		invid.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		invid.x	$$⊢\phi \to X\in B$$
5		eqid	$$⊢\mathrm{Inv}\left(C\right)=\mathrm{Inv}\left(C\right)$$
6	1 5 3 4 4	invfun	$$⊢\phi \to \mathrm{Fun}\left(X\mathrm{Inv}\left(C\right)X\right)$$
7	1 2 3 4	invid	$$⊢\phi \to I\left(X\right)\left(X\mathrm{Inv}\left(C\right)X\right)I\left(X\right)$$
8		funbrfv	$$⊢\mathrm{Fun}\left(X\mathrm{Inv}\left(C\right)X\right)\to \left(I\left(X\right)\left(X\mathrm{Inv}\left(C\right)X\right)I\left(X\right)\to \left(X\mathrm{Inv}\left(C\right)X\right)\left(I\left(X\right)\right)=I\left(X\right)\right)$$
9	6 7 8	sylc	$$⊢\phi \to \left(X\mathrm{Inv}\left(C\right)X\right)\left(I\left(X\right)\right)=I\left(X\right)$$