Theorem cicpropd

Description: Two structures with the same base, hom-sets and composition operation have the same isomorphic objects. (Contributed by Zhi Wang, 27-Oct-2025)

	Ref	Expression
Hypotheses	cicpropd.1	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
	cicpropd.2	|- ( ph -> ( comf ` C ) = ( comf ` D ) )
Assertion	cicpropd	|- ( ph -> ( ~=c ` C ) = ( ~=c ` D ) )

Proof

Step	Hyp	Ref	Expression
1		cicpropd.1	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2		cicpropd.2	|- ( ph -> ( comf ` C ) = ( comf ` D ) )
3	1 2	cicpropdlem	|- ( ( ph /\ f e. ( ~=c ` C ) ) -> f e. ( ~=c ` D ) )
4	1	eqcomd	|- ( ph -> ( Homf ` D ) = ( Homf ` C ) )
5	2	eqcomd	|- ( ph -> ( comf ` D ) = ( comf ` C ) )
6	4 5	cicpropdlem	|- ( ( ph /\ f e. ( ~=c ` D ) ) -> f e. ( ~=c ` C ) )
7	3 6	impbida	|- ( ph -> ( f e. ( ~=c ` C ) <-> f e. ( ~=c ` D ) ) )
8	7	eqrdv	|- ( ph -> ( ~=c ` C ) = ( ~=c ` D ) )