Metamath Proof Explorer

Theorem cicerALT

Description: Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in Adamek p. 29. (Contributed by AV, 5-Apr-2020) (Proof shortened by Zhi Wang, 3-Nov-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cicerALT 
|- ( C e. Cat -> ( ~=c ` C ) Er ( Base ` C ) )

Proof

Step Hyp Ref Expression
1 relcic 
 |-  ( C e. Cat -> Rel ( ~=c ` C ) )
2 cicsym 
 |-  ( ( C e. Cat /\ x ( ~=c ` C ) y ) -> y ( ~=c ` C ) x )
3 cictr 
 |-  ( ( C e. Cat /\ x ( ~=c ` C ) y /\ y ( ~=c ` C ) z ) -> x ( ~=c ` C ) z )
4 3 3expb 
 |-  ( ( C e. Cat /\ ( x ( ~=c ` C ) y /\ y ( ~=c ` C ) z ) ) -> x ( ~=c ` C ) z )
5 cicref 
 |-  ( ( C e. Cat /\ x e. ( Base ` C ) ) -> x ( ~=c ` C ) x )
6 ciclcl 
 |-  ( ( C e. Cat /\ x ( ~=c ` C ) x ) -> x e. ( Base ` C ) )
7 5 6 impbida 
 |-  ( C e. Cat -> ( x e. ( Base ` C ) <-> x ( ~=c ` C ) x ) )
8 1 2 4 7 iserd 
 |-  ( C e. Cat -> ( ~=c ` C ) Er ( Base ` C ) )