Theorem cicref

Description: Isomorphism is reflexive. (Contributed by AV, 5-Apr-2020)

	Ref	Expression
Assertion	cicref	$$⊢\left(C\in \mathrm{Cat}\wedge O\in {\mathrm{Base}}_C\right)\to O{\simeq }_{𝑐}\left(C\right)O$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{Iso}\left(C\right)=\mathrm{Iso}\left(C\right)$$
2		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
3		simpl	$$⊢\left(C\in \mathrm{Cat}\wedge O\in {\mathrm{Base}}_C\right)\to C\in \mathrm{Cat}$$
4		simpr	$$⊢\left(C\in \mathrm{Cat}\wedge O\in {\mathrm{Base}}_C\right)\to O\in {\mathrm{Base}}_C$$
5		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
6	2 5 3 4	idiso	$$⊢\left(C\in \mathrm{Cat}\wedge O\in {\mathrm{Base}}_C\right)\to \mathrm{Id}\left(C\right)\left(O\right)\in \left(O\mathrm{Iso}\left(C\right)O\right)$$
7	1 2 3 4 4 6	brcici	$$⊢\left(C\in \mathrm{Cat}\wedge O\in {\mathrm{Base}}_C\right)\to O{\simeq }_{𝑐}\left(C\right)O$$