Definition df-full

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)

	Ref	Expression
Assertion	df-full	$$⊢\mathrm{Full}=\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼\left\{⟨f,g⟩|\left(f\left(c\mathrm{Func}d\right)g\wedge \forall x\in {\mathrm{Base}}_c\forall y\in {\mathrm{Base}}_c\mathrm{ran}\left(xgy\right)=f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cful	$$class\mathrm{Full}$$
1		vc	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		vd	$$setvard$$
4		vf	$$setvarf$$
5		vg	$$setvarg$$
6	4	cv	$$setvarf$$
7	1	cv	$$setvarc$$
8		cfunc	$$class\mathrm{Func}$$
9	3	cv	$$setvard$$
10	7 9 8	co	$$class\left(c\mathrm{Func}d\right)$$
11	5	cv	$$setvarg$$
12	6 11 10	wbr	$$wfff\left(c\mathrm{Func}d\right)g$$
13		vx	$$setvarx$$
14		cbs	$$class\mathrm{Base}$$
15	7 14	cfv	$$class{\mathrm{Base}}_c$$
16		vy	$$setvary$$
17	13	cv	$$setvarx$$
18	16	cv	$$setvary$$
19	17 18 11	co	$$class\left(xgy\right)$$
20	19	crn	$$class\mathrm{ran}\left(xgy\right)$$
21	17 6	cfv	$$classf\left(x\right)$$
22		chom	$$class\mathrm{Hom}$$
23	9 22	cfv	$$class\mathrm{Hom}\left(d\right)$$
24	18 6	cfv	$$classf\left(y\right)$$
25	21 24 23	co	$$class\left(f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)\right)$$
26	20 25	wceq	$$wff\mathrm{ran}\left(xgy\right)=f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)$$
27	26 16 15	wral	$$wff\forall y\in {\mathrm{Base}}_c\mathrm{ran}\left(xgy\right)=f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)$$
28	27 13 15	wral	$$wff\forall x\in {\mathrm{Base}}_c\forall y\in {\mathrm{Base}}_c\mathrm{ran}\left(xgy\right)=f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)$$
29	12 28	wa	$$wff\left(f\left(c\mathrm{Func}d\right)g\wedge \forall x\in {\mathrm{Base}}_c\forall y\in {\mathrm{Base}}_c\mathrm{ran}\left(xgy\right)=f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)\right)$$
30	29 4 5	copab	$$class\left\{⟨f,g⟩|\left(f\left(c\mathrm{Func}d\right)g\wedge \forall x\in {\mathrm{Base}}_c\forall y\in {\mathrm{Base}}_c\mathrm{ran}\left(xgy\right)=f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)\right)\right\}$$
31	1 3 2 2 30	cmpo	$$class\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼\left\{⟨f,g⟩|\left(f\left(c\mathrm{Func}d\right)g\wedge \forall x\in {\mathrm{Base}}_c\forall y\in {\mathrm{Base}}_c\mathrm{ran}\left(xgy\right)=f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)\right)\right\}\right)$$
32	0 31	wceq	$$wff\mathrm{Full}=\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼\left\{⟨f,g⟩|\left(f\left(c\mathrm{Func}d\right)g\wedge \forall x\in {\mathrm{Base}}_c\forall y\in {\mathrm{Base}}_c\mathrm{ran}\left(xgy\right)=f\left(x\right)\mathrm{Hom}\left(d\right)f\left(y\right)\right)\right\}\right)$$