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={\mathrm{Base}}_C$$
	isoco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	isoco.n	$$⊢I=\mathrm{Iso}\left(C\right)$$
	isoco.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	isoco.x	$$⊢\phi \to X\in B$$
	isoco.y	$$⊢\phi \to Y\in B$$
	isoco.z	$$⊢\phi \to Z\in B$$
	isoco.f	$$⊢\phi \to F\in \left(XIY\right)$$
	isoco.g	$$⊢\phi \to G\in \left(YIZ\right)$$
Assertion	isoco	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left(XIZ\right)$$

Proof

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