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

Metamath Proof Explorer

Theorem homahom2

Description: The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homahom.h ⊢ H = Hom a ⁡ C
homahom.j ⊢ J = Hom ⁡ C
Assertion homahom2 ⊢ Z X H Y F → F ∈ X J Y

Proof

Step Hyp Ref Expression
1 homahom.h ⊢ H = Hom a ⁡ C
2 homahom.j ⊢ J = Hom ⁡ C
3 df-br ⊢ Z X H Y F ↔ Z F ∈ X H Y
4 eqid ⊢ Base C = Base C
5 1 homarcl ⊢ Z F ∈ X H Y → C ∈ Cat
6 1 4 homarcl2 ⊢ Z F ∈ X H Y → X ∈ Base C ∧ Y ∈ Base C
7 6 simpld ⊢ Z F ∈ X H Y → X ∈ Base C
8 6 simprd ⊢ Z F ∈ X H Y → Y ∈ Base C
9 1 4 5 2 7 8 elhoma ⊢ Z F ∈ X H Y → Z X H Y F ↔ Z = X Y ∧ F ∈ X J Y
10 3 9 sylbi ⊢ Z X H Y F → Z X H Y F ↔ Z = X Y ∧ F ∈ X J Y
11 10 ibi ⊢ Z X H Y F → Z = X Y ∧ F ∈ X J Y
12 11 simprd ⊢ Z X H Y F → F ∈ X J Y