Metamath Proof Explorer


Theorem monhom

Description: A monomorphism is a morphism. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses ismon.b B=BaseC
ismon.h H=HomC
ismon.o ·˙=compC
ismon.s M=MonoC
ismon.c φCCat
ismon.x φXB
ismon.y φYB
Assertion monhom φXMYXHY

Proof

Step Hyp Ref Expression
1 ismon.b B=BaseC
2 ismon.h H=HomC
3 ismon.o ·˙=compC
4 ismon.s M=MonoC
5 ismon.c φCCat
6 ismon.x φXB
7 ismon.y φYB
8 1 2 3 4 5 6 7 ismon φfXMYfXHYzBFungzHXfzX·˙Yg-1
9 simpl fXHYzBFungzHXfzX·˙Yg-1fXHY
10 8 9 syl6bi φfXMYfXHY
11 10 ssrdv φXMYXHY