Definition df-fth 16565

Description: Function returning all the faithful functors from a category C to a category D. A full 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.)

Assertion

Ref	Expression
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 ) ) } )

Distinct variable group:   c, d, f, g, x, y

Detailed syntax breakdown of Definition df-fth

Step	Hyp	Ref	Expression
1		cfth 16563	. 2 class Faith
2		vc	. . 3 setvar c
3		vd	. . 3 setvar d
4		ccat 16325	. . 3 class Cat
5		vf	. . . . . . 7 setvar f
6	5	cv 1482	. . . . . 6 class f
7		vg	. . . . . . 7 setvar g
8	7	cv 1482	. . . . . 6 class g
9	2	cv 1482	. . . . . . 7 class c
10	3	cv 1482	. . . . . . 7 class d
11		cfunc 16514	. . . . . . 7 class Func
12	9, 10, 11	co 6650	. . . . . 6 class ( c Func d )
13	6, 8, 12	wbr 4653	. . . . 5 wff f ( c Func d ) g
14		vx	. . . . . . . . . . 11 setvar x
15	14	cv 1482	. . . . . . . . . 10 class x
16		vy	. . . . . . . . . . 11 setvar y
17	16	cv 1482	. . . . . . . . . 10 class y
18	15, 17, 8	co 6650	. . . . . . . . 9 class ( x g y )
19	18	ccnv 5113	. . . . . . . 8 class `' ( x g y )
20	19	wfun 5882	. . . . . . 7 wff Fun `' ( x g y )
21		cbs 15857	. . . . . . . 8 class Base
22	9, 21	cfv 5888	. . . . . . 7 class ( Base ` c )
23	20, 16, 22	wral 2912	. . . . . 6 wff A. y e. ( Base ` c ) Fun `' ( x g y )
24	23, 14, 22	wral 2912	. . . . 5 wff A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y )
25	13, 24	wa 384	. . . 4 wff ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) )
26	25, 5, 7	copab 4712	. . 3 class { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) }
27	2, 3, 4, 4, 26	cmpt2 6652	. 2 class ( 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 ) ) } )
28	1, 27	wceq 1483	1 wff 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 ) ) } )

This definition is referenced by:  fthfunc  16567  isfth  16574