Metamath Proof Explorer

Theorem cicer

Description: Isomorphism is an equivalence relation on objects of a category. Remark 3.16 in Adamek p. 29. (Contributed by AV, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 relopabv 
 |-  Rel { <. x , y >. | ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ ( ( Iso ` C ) ` <. x , y >. ) =/= (/) ) }
2 1 a1i 
 |-  ( C e. Cat -> Rel { <. x , y >. | ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ ( ( Iso ` C ) ` <. x , y >. ) =/= (/) ) } )
3 fveq2 
 |-  ( f = <. x , y >. -> ( ( Iso ` C ) ` f ) = ( ( Iso ` C ) ` <. x , y >. ) )
4 3 neeq1d 
 |-  ( f = <. x , y >. -> ( ( ( Iso ` C ) ` f ) =/= (/) <-> ( ( Iso ` C ) ` <. x , y >. ) =/= (/) ) )
5 4 rabxp 
 |-  { f e. ( ( Base ` C ) X. ( Base ` C ) ) | ( ( Iso ` C ) ` f ) =/= (/) } = { <. x , y >. | ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ ( ( Iso ` C ) ` <. x , y >. ) =/= (/) ) }
6 5 a1i 
 |-  ( C e. Cat -> { f e. ( ( Base ` C ) X. ( Base ` C ) ) | ( ( Iso ` C ) ` f ) =/= (/) } = { <. x , y >. | ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ ( ( Iso ` C ) ` <. x , y >. ) =/= (/) ) } )
7 6 releqd 
 |-  ( C e. Cat -> ( Rel { f e. ( ( Base ` C ) X. ( Base ` C ) ) | ( ( Iso ` C ) ` f ) =/= (/) } <-> Rel { <. x , y >. | ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ ( ( Iso ` C ) ` <. x , y >. ) =/= (/) ) } ) )
8 2 7 mpbird 
 |-  ( C e. Cat -> Rel { f e. ( ( Base ` C ) X. ( Base ` C ) ) | ( ( Iso ` C ) ` f ) =/= (/) } )
9 isofn 
 |-  ( C e. Cat -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
10 fvex 
 |-  ( Base ` C ) e. _V
11 sqxpexg 
 |-  ( ( Base ` C ) e. _V -> ( ( Base ` C ) X. ( Base ` C ) ) e. _V )
12 10 11 mp1i 
 |-  ( C e. Cat -> ( ( Base ` C ) X. ( Base ` C ) ) e. _V )
13 0ex 
 |-  (/) e. _V
14 13 a1i 
 |-  ( C e. Cat -> (/) e. _V )
15 suppvalfn 
 |-  ( ( ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ ( ( Base ` C ) X. ( Base ` C ) ) e. _V /\ (/) e. _V ) -> ( ( Iso ` C ) supp (/) ) = { f e. ( ( Base ` C ) X. ( Base ` C ) ) | ( ( Iso ` C ) ` f ) =/= (/) } )
16 9 12 14 15 syl3anc 
 |-  ( C e. Cat -> ( ( Iso ` C ) supp (/) ) = { f e. ( ( Base ` C ) X. ( Base ` C ) ) | ( ( Iso ` C ) ` f ) =/= (/) } )
17 16 releqd 
 |-  ( C e. Cat -> ( Rel ( ( Iso ` C ) supp (/) ) <-> Rel { f e. ( ( Base ` C ) X. ( Base ` C ) ) | ( ( Iso ` C ) ` f ) =/= (/) } ) )
18 8 17 mpbird 
 |-  ( C e. Cat -> Rel ( ( Iso ` C ) supp (/) ) )
19 cicfval 
 |-  ( C e. Cat -> ( ~=c ` C ) = ( ( Iso ` C ) supp (/) ) )
20 19 releqd 
 |-  ( C e. Cat -> ( Rel ( ~=c ` C ) <-> Rel ( ( Iso ` C ) supp (/) ) ) )
21 18 20 mpbird 
 |-  ( C e. Cat -> Rel ( ~=c ` C ) )
22 cicsym 
 |-  ( ( C e. Cat /\ x ( ~=c ` C ) y ) -> y ( ~=c ` C ) x )
23 cictr 
 |-  ( ( C e. Cat /\ x ( ~=c ` C ) y /\ y ( ~=c ` C ) z ) -> x ( ~=c ` C ) z )
24 23 3expb 
 |-  ( ( C e. Cat /\ ( x ( ~=c ` C ) y /\ y ( ~=c ` C ) z ) ) -> x ( ~=c ` C ) z )
25 cicref 
 |-  ( ( C e. Cat /\ x e. ( Base ` C ) ) -> x ( ~=c ` C ) x )
26 ciclcl 
 |-  ( ( C e. Cat /\ x ( ~=c ` C ) x ) -> x e. ( Base ` C ) )
27 25 26 impbida 
 |-  ( C e. Cat -> ( x e. ( Base ` C ) <-> x ( ~=c ` C ) x ) )
28 21 22 24 27 iserd 
 |-  ( C e. Cat -> ( ~=c ` C ) Er ( Base ` C ) )