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	|- .x. = ( comp ` C )
	isoco.n	|- I = ( Iso ` C )
	isoco.c	|- ( ph -> C e. Cat )
	isoco.x	|- ( ph -> X e. B )
	isoco.y	|- ( ph -> Y e. B )
	isoco.z	|- ( ph -> Z e. B )
	isoco.f	|- ( ph -> F e. ( X I Y ) )
	isoco.g	|- ( ph -> G e. ( Y I Z ) )
Assertion	isoco	|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X I Z ) )

Proof

Step	Hyp	Ref	Expression
1		isoco.b	|- B = ( Base ` C )
2		isoco.o	|- .x. = ( comp ` C )
3		isoco.n	|- I = ( Iso ` C )
4		isoco.c	|- ( ph -> C e. Cat )
5		isoco.x	|- ( ph -> X e. B )
6		isoco.y	|- ( ph -> Y e. B )
7		isoco.z	|- ( ph -> Z e. B )
8		isoco.f	|- ( ph -> F e. ( X I Y ) )
9		isoco.g	|- ( ph -> G e. ( Y I Z ) )
10		eqid	|- ( Inv ` C ) = ( Inv ` C )
11	1 10 4 5 6 3 8 2 7 9	invco	|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) ( X ( Inv ` C ) Z ) ( ( ( X ( Inv ` C ) Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y ( Inv ` C ) Z ) ` G ) ) )
12	1 10 4 5 7 3 11	inviso1	|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X I Z ) )