Definition df-full 16564

Description: Function returning all the full 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 surjections. Definition 3.27(3) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.)

Assertion

Ref	Expression
df-full	|- Full = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )

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

Detailed syntax breakdown of Definition df-full

Step	Hyp	Ref	Expression
1		cful 16562	. 2 class Full
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	crn 5115	. . . . . . . 8 class ran ( x g y )
20	15, 6	cfv 5888	. . . . . . . . 9 class ( f ` x )
21	17, 6	cfv 5888	. . . . . . . . 9 class ( f ` y )
22		chom 15952	. . . . . . . . . 10 class Hom
23	10, 22	cfv 5888	. . . . . . . . 9 class ( Hom ` d )
24	20, 21, 23	co 6650	. . . . . . . 8 class ( ( f ` x ) ( Hom ` d ) ( f ` y ) )
25	19, 24	wceq 1483	. . . . . . 7 wff ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) )
26		cbs 15857	. . . . . . . 8 class Base
27	9, 26	cfv 5888	. . . . . . 7 class ( Base ` c )
28	25, 16, 27	wral 2912	. . . . . 6 wff A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) )
29	28, 14, 27	wral 2912	. . . . 5 wff A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) )
30	13, 29	wa 384	. . . 4 wff ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) )
31	30, 5, 7	copab 4712	. . 3 class { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) }
32	2, 3, 4, 4, 31	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 ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )
33	1, 32	wceq 1483	1 wff Full = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )

This definition is referenced by:  fullfunc  16566  isfull  16570