Theorem epihom

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

	Ref	Expression
Hypotheses	isepi.b	|- B = ( Base ` C )
	isepi.h	|- H = ( Hom ` C )
	isepi.o	|- .x. = ( comp ` C )
	isepi.e	|- E = ( Epi ` C )
	isepi.c	|- ( ph -> C e. Cat )
	isepi.x	|- ( ph -> X e. B )
	isepi.y	|- ( ph -> Y e. B )
Assertion	epihom	|- ( ph -> ( X E Y ) C_ ( X H Y ) )

Proof

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