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	⊢ 𝐵 = ( Base ‘ 𝐶 )
	isoco.o	⊢ · = ( comp ‘ 𝐶 )
	isoco.n	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	isoco.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	isoco.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	isoco.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	isoco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	isoco.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
	isoco.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐼 𝑍 ) )
Assertion	isoco	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐼 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		isoco.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isoco.o	⊢ · = ( comp ‘ 𝐶 )
3		isoco.n	⊢ 𝐼 = ( Iso ‘ 𝐶 )
4		isoco.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		isoco.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		isoco.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		isoco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		isoco.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
9		isoco.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐼 𝑍 ) )
10		eqid	⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
11	1 10 4 5 6 3 8 2 7 9	invco	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 ( Inv ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 ( Inv ‘ 𝐶 ) 𝑍 ) ‘ 𝐺 ) ) )
12	1 10 4 5 7 3 11	inviso1	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐼 𝑍 ) )