Metamath Proof Explorer

Theorem homdmcoa

Description: If F : X --> Y and G : Y --> Z , then G and F are composable. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homdmcoa.o ⊢ · ˙ = comp a ⁡ C
homdmcoa.h ⊢ H = Hom a ⁡ C
homdmcoa.f ⊢ φ → F ∈ X H Y
homdmcoa.g ⊢ φ → G ∈ Y H Z
Assertion homdmcoa ⊢ φ → G dom ⁡ · ˙ F

Proof

Step Hyp Ref Expression
1 homdmcoa.o ⊢ · ˙ = comp a ⁡ C
2 homdmcoa.h ⊢ H = Hom a ⁡ C
3 homdmcoa.f ⊢ φ → F ∈ X H Y
4 homdmcoa.g ⊢ φ → G ∈ Y H Z
5 eqid ⊢ Arrow ⁡ C = Arrow ⁡ C
6 5 2 homarw ⊢ X H Y ⊆ Arrow ⁡ C
7 6 3 sseldi ⊢ φ → F ∈ Arrow ⁡ C
8 5 2 homarw ⊢ Y H Z ⊆ Arrow ⁡ C
9 8 4 sseldi ⊢ φ → G ∈ Arrow ⁡ C
10 2 homacd ⊢ F ∈ X H Y → cod a ⁡ F = Y
11 3 10 syl ⊢ φ → cod a ⁡ F = Y
12 2 homadm ⊢ G ∈ Y H Z → dom a ⁡ G = Y
13 4 12 syl ⊢ φ → dom a ⁡ G = Y
14 11 13 eqtr4d ⊢ φ → cod a ⁡ F = dom a ⁡ G
15 1 5 eldmcoa ⊢ G dom ⁡ · ˙ F ↔ F ∈ Arrow ⁡ C ∧ G ∈ Arrow ⁡ C ∧ cod a ⁡ F = dom a ⁡ G
16 7 9 14 15 syl3anbrc ⊢ φ → G dom ⁡ · ˙ F