Theorem monhom

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

	Ref	Expression
Hypotheses	ismon.b	|- B = ( Base ` C )
	ismon.h	|- H = ( Hom ` C )
	ismon.o	|- .x. = ( comp ` C )
	ismon.s	|- M = ( Mono ` C )
	ismon.c	|- ( ph -> C e. Cat )
	ismon.x	|- ( ph -> X e. B )
	ismon.y	|- ( ph -> Y e. B )
Assertion	monhom	|- ( ph -> ( X M Y ) C_ ( X H Y ) )

Proof

Step	Hyp	Ref	Expression
1		ismon.b	|- B = ( Base ` C )
2		ismon.h	|- H = ( Hom ` C )
3		ismon.o	|- .x. = ( comp ` C )
4		ismon.s	|- M = ( Mono ` C )
5		ismon.c	|- ( ph -> C e. Cat )
6		ismon.x	|- ( ph -> X e. B )
7		ismon.y	|- ( ph -> Y e. B )
8	1 2 3 4 5 6 7	ismon	|- ( ph -> ( f e. ( X M Y ) <-> ( f e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) ) ) )
9		simpl	|- ( ( f e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) ) -> f e. ( X H Y ) )
10	8 9	biimtrdi	|- ( ph -> ( f e. ( X M Y ) -> f e. ( X H Y ) ) )
11	10	ssrdv	|- ( ph -> ( X M Y ) C_ ( X H Y ) )