Theorem invpropd

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

	Ref	Expression
Hypotheses	sectpropd.1	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
	sectpropd.2	|- ( ph -> ( comf ` C ) = ( comf ` D ) )
Assertion	invpropd	|- ( ph -> ( Inv ` C ) = ( Inv ` D ) )

Proof

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