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 ) |
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 ) |