Metamath Proof Explorer

Theorem relcic

Description: The set of isomorphic objects is a relation. Simplifies cicer (see cicerALT ). (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion relcic 
|- ( C e. Cat -> Rel ( ~=c ` C ) )

Proof

Step Hyp Ref Expression
1 relopab 
 |-  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 ) )