Metamath Proof Explorer

Theorem homa1

Description: The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypothesis homahom.h ⊢ H = Hom a ⁡ C
Assertion homa1 ⊢ Z X H Y F → Z = X Y

Proof

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