Description: Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | homarcl.h | |- H = ( HomA ` C ) |
|
| homafval.b | |- B = ( Base ` C ) |
||
| homafval.c | |- ( ph -> C e. Cat ) |
||
| homaval.j | |- J = ( Hom ` C ) |
||
| homaval.x | |- ( ph -> X e. B ) |
||
| homaval.y | |- ( ph -> Y e. B ) |
||
| elhomai.f | |- ( ph -> F e. ( X J Y ) ) |
||
| Assertion | elhomai | |- ( ph -> <. X , Y >. ( X H Y ) F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | homarcl.h | |- H = ( HomA ` C ) |
|
| 2 | homafval.b | |- B = ( Base ` C ) |
|
| 3 | homafval.c | |- ( ph -> C e. Cat ) |
|
| 4 | homaval.j | |- J = ( Hom ` C ) |
|
| 5 | homaval.x | |- ( ph -> X e. B ) |
|
| 6 | homaval.y | |- ( ph -> Y e. B ) |
|
| 7 | elhomai.f | |- ( ph -> F e. ( X J Y ) ) |
|
| 8 | eqidd | |- ( ph -> <. X , Y >. = <. X , Y >. ) |
|
| 9 | 1 2 3 4 5 6 | elhoma | |- ( ph -> ( <. X , Y >. ( X H Y ) F <-> ( <. X , Y >. = <. X , Y >. /\ F e. ( X J Y ) ) ) ) |
| 10 | 8 7 9 | mpbir2and | |- ( ph -> <. X , Y >. ( X H Y ) F ) |