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	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	cicpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
Assertion	cicpropd	$$⊢\phi \to {\simeq }_{𝑐}\left(C\right)={\simeq }_{𝑐}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		cicpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
2		cicpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
3	1 2	cicpropdlem	$$⊢\left(\phi \wedge f\in {\simeq }_{𝑐}\left(C\right)\right)\to f\in {\simeq }_{𝑐}\left(D\right)$$
4	1	eqcomd	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
5	2	eqcomd	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(C\right)$$
6	4 5	cicpropdlem	$$⊢\left(\phi \wedge f\in {\simeq }_{𝑐}\left(D\right)\right)\to f\in {\simeq }_{𝑐}\left(C\right)$$
7	3 6	impbida	$$⊢\phi \to \left(f\in {\simeq }_{𝑐}\left(C\right)\leftrightarrow f\in {\simeq }_{𝑐}\left(D\right)\right)$$
8	7	eqrdv	$$⊢\phi \to {\simeq }_{𝑐}\left(C\right)={\simeq }_{𝑐}\left(D\right)$$