Theorem invid

Description: The inverse of the identity is the identity. (Contributed by AV, 8-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	invid	$$⊢\phi \to I\left(X\right)\left(X\mathrm{Inv}\left(C\right)X\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	1 2 3 4	sectid	$$⊢\phi \to I\left(X\right)\left(X\mathrm{Sect}\left(C\right)X\right)I\left(X\right)$$
6		eqid	$$⊢\mathrm{Inv}\left(C\right)=\mathrm{Inv}\left(C\right)$$
7		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
8	1 6 3 4 4 7	isinv	$$⊢\phi \to \left(I\left(X\right)\left(X\mathrm{Inv}\left(C\right)X\right)I\left(X\right)\leftrightarrow \left(I\left(X\right)\left(X\mathrm{Sect}\left(C\right)X\right)I\left(X\right)\wedge I\left(X\right)\left(X\mathrm{Sect}\left(C\right)X\right)I\left(X\right)\right)\right)$$
9	5 5 8	mpbir2and	$$⊢\phi \to I\left(X\right)\left(X\mathrm{Inv}\left(C\right)X\right)I\left(X\right)$$