Theorem cicref

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

	Ref	Expression
Assertion	cicref	|- ( ( C e. Cat /\ O e. ( Base ` C ) ) -> O ( ~=c ` C ) O )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Iso ` C ) = ( Iso ` C )
2		eqid	|- ( Base ` C ) = ( Base ` C )
3		simpl	|- ( ( C e. Cat /\ O e. ( Base ` C ) ) -> C e. Cat )
4		simpr	|- ( ( C e. Cat /\ O e. ( Base ` C ) ) -> O e. ( Base ` C ) )
5		eqid	|- ( Id ` C ) = ( Id ` C )
6	2 5 3 4	idiso	|- ( ( C e. Cat /\ O e. ( Base ` C ) ) -> ( ( Id ` C ) ` O ) e. ( O ( Iso ` C ) O ) )
7	1 2 3 4 4 6	brcici	|- ( ( C e. Cat /\ O e. ( Base ` C ) ) -> O ( ~=c ` C ) O )