Theorem idiso

Description: The identity is an isomorphism. Example 3.13 of Adamek p. 28. (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	idiso	$$⊢\phi \to I\left(X\right)\in \left(X\mathrm{Iso}\left(C\right)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		eqid	$$⊢\mathrm{Iso}\left(C\right)=\mathrm{Iso}\left(C\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	1 5 3 4 4 6 7	inviso1	$$⊢\phi \to I\left(X\right)\in \left(X\mathrm{Iso}\left(C\right)X\right)$$