Definition df-full 16387

Description: Function returning all the full functors from a category 𝐶 to a category 𝐷. A full functor is a functor in which all the morphism maps 𝐺(𝑋, 𝑌) between objects 𝑋, 𝑌 ∈ 𝐶 are surjections. Definition 3.27(3) in [Adamek] p. 34. (Contributed by Mario Carneiro, 26-Jan-2017.)

Assertion

Ref	Expression
df-full	⊢ Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})

Distinct variable group:   𝑐,𝑑,𝑓,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-full

Step	Hyp	Ref	Expression
1		cful 16385	. 2 class Full
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		ccat 16148	. . 3 class Cat
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1474	. . . . . 6 class 𝑓
7		vg	. . . . . . 7 setvar 𝑔
8	7	cv 1474	. . . . . 6 class 𝑔
9	2	cv 1474	. . . . . . 7 class 𝑐
10	3	cv 1474	. . . . . . 7 class 𝑑
11		cfunc 16337	. . . . . . 7 class Func
12	9, 10, 11	co 6549	. . . . . 6 class (𝑐 Func 𝑑)
13	6, 8, 12	wbr 4583	. . . . 5 wff 𝑓(𝑐 Func 𝑑)𝑔
14		vx	. . . . . . . . . . 11 setvar 𝑥
15	14	cv 1474	. . . . . . . . . 10 class 𝑥
16		vy	. . . . . . . . . . 11 setvar 𝑦
17	16	cv 1474	. . . . . . . . . 10 class 𝑦
18	15, 17, 8	co 6549	. . . . . . . . 9 class (𝑥𝑔𝑦)
19	18	crn 5039	. . . . . . . 8 class ran (𝑥𝑔𝑦)
20	15, 6	cfv 5804	. . . . . . . . 9 class (𝑓‘𝑥)
21	17, 6	cfv 5804	. . . . . . . . 9 class (𝑓‘𝑦)
22		chom 15779	. . . . . . . . . 10 class Hom
23	10, 22	cfv 5804	. . . . . . . . 9 class (Hom ‘𝑑)
24	20, 21, 23	co 6549	. . . . . . . 8 class ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))
25	19, 24	wceq 1475	. . . . . . 7 wff ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))
26		cbs 15695	. . . . . . . 8 class Base
27	9, 26	cfv 5804	. . . . . . 7 class (Base‘𝑐)
28	25, 16, 27	wral 2896	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))
29	28, 14, 27	wral 2896	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))
30	13, 29	wa 383	. . . 4 wff (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))
31	30, 5, 7	copab 4642	. . 3 class {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))}
32	2, 3, 4, 4, 31	cmpt2 6551	. 2 class (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
33	1, 32	wceq 1475	1 wff Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})

This definition is referenced by:  fullfunc  16389  isfull  16393