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

Metamath Proof Explorer

Theorem isoco

Description: The composition of two isomorphisms is an isomorphism. Proposition 3.14(2) of Adamek p. 29. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Hypotheses	isoco.b	$⊢ B = {Base}_{C}$
		isoco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
		isoco.n	$⊢ I = Iso (C)$
		isoco.c	$⊢ φ \to C \in Cat$
		isoco.x	$⊢ φ \to X \in B$
		isoco.y	$⊢ φ \to Y \in B$
		isoco.z	$⊢ φ \to Z \in B$
		isoco.f	$⊢ φ \to F \in (X I Y)$
		isoco.g	$⊢ φ \to G \in (Y I Z)$
	Assertion	isoco	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X I Z)$

Proof

Step	Hyp	Ref	Expression
1		isoco.b	$⊢ B = {Base}_{C}$
2		isoco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
3		isoco.n	$⊢ I = Iso (C)$
4		isoco.c	$⊢ φ \to C \in Cat$
5		isoco.x	$⊢ φ \to X \in B$
6		isoco.y	$⊢ φ \to Y \in B$
7		isoco.z	$⊢ φ \to Z \in B$
8		isoco.f	$⊢ φ \to F \in (X I Y)$
9		isoco.g	$⊢ φ \to G \in (Y I Z)$
10		eqid	$⊢ Inv (C) = Inv (C)$
11	1 10 4 5 6 3 8 2 7 9	invco	$⊢ φ \to (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (X Inv (C) Z) ((X Inv (C) Y) (F) (⟨Z, Y⟩ \underset{˙}{\cdot} X) (Y Inv (C) Z) (G))$
12	1 10 4 5 7 3 11	inviso1	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F \in (X I Z)$