Theorem fulli

Description: The morphism map of a full functor is a surjection. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	isfull.b	|- B = ( Base ` C )
	isfull.j	|- J = ( Hom ` D )
	isfull.h	|- H = ( Hom ` C )
	fullfo.f	|- ( ph -> F ( C Full D ) G )
	fullfo.x	|- ( ph -> X e. B )
	fullfo.y	|- ( ph -> Y e. B )
	fulli.r	|- ( ph -> R e. ( ( F ` X ) J ( F ` Y ) ) )
Assertion	fulli	|- ( ph -> E. f e. ( X H Y ) R = ( ( X G Y ) ` f ) )

Proof

Step	Hyp	Ref	Expression
1		isfull.b	|- B = ( Base ` C )
2		isfull.j	|- J = ( Hom ` D )
3		isfull.h	|- H = ( Hom ` C )
4		fullfo.f	|- ( ph -> F ( C Full D ) G )
5		fullfo.x	|- ( ph -> X e. B )
6		fullfo.y	|- ( ph -> Y e. B )
7		fulli.r	|- ( ph -> R e. ( ( F ` X ) J ( F ` Y ) ) )
8	1 2 3 4 5 6	fullfo	|- ( ph -> ( X G Y ) : ( X H Y ) -onto-> ( ( F ` X ) J ( F ` Y ) ) )
9		foelrn	|- ( ( ( X G Y ) : ( X H Y ) -onto-> ( ( F ` X ) J ( F ` Y ) ) /\ R e. ( ( F ` X ) J ( F ` Y ) ) ) -> E. f e. ( X H Y ) R = ( ( X G Y ) ` f ) )
10	8 7 9	syl2anc	|- ( ph -> E. f e. ( X H Y ) R = ( ( X G Y ) ` f ) )