Metamath Proof Explorer

Theorem cicrcl2

Description: Isomorphism implies the structure being a category. (Contributed by Zhi Wang, 26-Oct-2025)

Ref Expression
Assertion cicrcl2 
|- ( R ( ~=c ` C ) S -> C e. Cat )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( R ( ~=c ` C ) S <-> <. R , S >. e. ( ~=c ` C ) )
2 elfvdm 
 |-  ( <. R , S >. e. ( ~=c ` C ) -> C e. dom ~=c )
3 cicfn 
 |-  ~=c Fn Cat
4 3 fndmi 
 |-  dom ~=c = Cat
5 2 4 eleqtrdi 
 |-  ( <. R , S >. e. ( ~=c ` C ) -> C e. Cat )
6 1 5 sylbi 
 |-  ( R ( ~=c ` C ) S -> C e. Cat )