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

Metamath Proof Explorer

Theorem elhomai

Description: Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homarcl.h ⊢ H = Hom a ⁡ C
homafval.b ⊢ B = Base C
homafval.c ⊢ φ → C ∈ Cat
homaval.j ⊢ J = Hom ⁡ C
homaval.x ⊢ φ → X ∈ B
homaval.y ⊢ φ → Y ∈ B
elhomai.f ⊢ φ → F ∈ X J Y
Assertion elhomai ⊢ φ → X Y X H Y F

Proof

Step Hyp Ref Expression
1 homarcl.h ⊢ H = Hom a ⁡ C
2 homafval.b ⊢ B = Base C
3 homafval.c ⊢ φ → C ∈ Cat
4 homaval.j ⊢ J = Hom ⁡ C
5 homaval.x ⊢ φ → X ∈ B
6 homaval.y ⊢ φ → Y ∈ B
7 elhomai.f ⊢ φ → F ∈ X J Y
8 eqidd ⊢ φ → X Y = X Y
9 1 2 3 4 5 6 elhoma ⊢ φ → X Y X H Y F ↔ X Y = X Y ∧ F ∈ X J Y
10 8 7 9 mpbir2and ⊢ φ → X Y X H Y F