Theorem sectid

Description: The identity is a section of itself. (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	sectid	$$⊢\phi \to I\left(X\right)\left(X\mathrm{Sect}\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		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
6		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
7	1 5 2 3 4	catidcl	$$⊢\phi \to I\left(X\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)$$
8	1 5 2 3 4 6 4 7	catlid	$$⊢\phi \to I\left(X\right)\left(⟨X,X⟩\mathrm{comp}\left(C\right)X\right)I\left(X\right)=I\left(X\right)$$
9		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
10	1 5 6 2 9 3 4 4 7 7	issect2	$$⊢\phi \to \left(I\left(X\right)\left(X\mathrm{Sect}\left(C\right)X\right)I\left(X\right)\leftrightarrow I\left(X\right)\left(⟨X,X⟩\mathrm{comp}\left(C\right)X\right)I\left(X\right)=I\left(X\right)\right)$$
11	8 10	mpbird	$$⊢\phi \to I\left(X\right)\left(X\mathrm{Sect}\left(C\right)X\right)I\left(X\right)$$