This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isopropd

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

		Ref	Expression
	Hypotheses	sectpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
		sectpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
	Assertion	isopropd	$⊢ φ \to Iso (C) = Iso (D)$

Proof

Step	Hyp	Ref	Expression
1		sectpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
2		sectpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
3	1 2	isopropdlem	$⊢ (φ \land f \in Iso (C)) \to f \in Iso (D)$
4	1	eqcomd	$⊢ φ \to {Hom}_{𝑓} (D) = {Hom}_{𝑓} (C)$
5	2	eqcomd	$⊢ φ \to {comp}_{𝑓} (D) = {comp}_{𝑓} (C)$
6	4 5	isopropdlem	$⊢ (φ \land f \in Iso (D)) \to f \in Iso (C)$
7	3 6	impbida	$⊢ φ \to (f \in Iso (C) \leftrightarrow f \in Iso (D))$
8	7	eqrdv	$⊢ φ \to Iso (C) = Iso (D)$