Metamath Proof Explorer


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 )