Definition df-fth

Description: Function returning all the faithful functors from a category C to a category D . A faithful functor is a functor in which all the morphism maps G ( X , Y ) between objects X , Y e. C are injections. Definition 3.27(2) in Adamek p. 34. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Assertion	df-fth	|- Faith = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfth	|- Faith
1		vc	|- c
2		ccat	|- Cat
3		vd	|- d
4		vf	|- f
5		vg	|- g
6	4	cv	|- f
7	1	cv	|- c
8		cfunc	|- Func
9	3	cv	|- d
10	7 9 8	co	|- ( c Func d )
11	5	cv	|- g
12	6 11 10	wbr	|- f ( c Func d ) g
13		vx	|- x
14		cbs	|- Base
15	7 14	cfv	|- ( Base ` c )
16		vy	|- y
17	13	cv	|- x
18	16	cv	|- y
19	17 18 11	co	|- ( x g y )
20	19	ccnv	|- `' ( x g y )
21	20	wfun	|- Fun `' ( x g y )
22	21 16 15	wral	|- A. y e. ( Base ` c ) Fun `' ( x g y )
23	22 13 15	wral	|- A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y )
24	12 23	wa	|- ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) )
25	24 4 5	copab	|- { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) }
26	1 3 2 2 25	cmpo	|- ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } )
27	0 26	wceq	|- Faith = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } )