Definition df-full 17620

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 17618	. 2 class Full
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		ccat 17373	. . 3 class Cat
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1538	. . . . . 6 class 𝑓
7		vg	. . . . . . 7 setvar 𝑔
8	7	cv 1538	. . . . . 6 class 𝑔
9	2	cv 1538	. . . . . . 7 class 𝑐
10	3	cv 1538	. . . . . . 7 class 𝑑
11		cfunc 17569	. . . . . . 7 class Func
12	9, 10, 11	co 7275	. . . . . 6 class (𝑐 Func 𝑑)
13	6, 8, 12	wbr 5074	. . . . 5 wff 𝑓(𝑐 Func 𝑑)𝑔
14		vx	. . . . . . . . . . 11 setvar 𝑥
15	14	cv 1538	. . . . . . . . . 10 class 𝑥
16		vy	. . . . . . . . . . 11 setvar 𝑦
17	16	cv 1538	. . . . . . . . . 10 class 𝑦
18	15, 17, 8	co 7275	. . . . . . . . 9 class (𝑥𝑔𝑦)
19	18	crn 5590	. . . . . . . 8 class ran (𝑥𝑔𝑦)
20	15, 6	cfv 6433	. . . . . . . . 9 class (𝑓‘𝑥)
21	17, 6	cfv 6433	. . . . . . . . 9 class (𝑓‘𝑦)
22		chom 16973	. . . . . . . . . 10 class Hom
23	10, 22	cfv 6433	. . . . . . . . 9 class (Hom ‘𝑑)
24	20, 21, 23	co 7275	. . . . . . . 8 class ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))
25	19, 24	wceq 1539	. . . . . . 7 wff ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))
26		cbs 16912	. . . . . . . 8 class Base
27	9, 26	cfv 6433	. . . . . . 7 class (Base‘𝑐)
28	25, 16, 27	wral 3064	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))
29	28, 14, 27	wral 3064	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))
30	13, 29	wa 396	. . . 4 wff (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))
31	30, 5, 7	copab 5136	. . 3 class {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))}
32	2, 3, 4, 4, 31	cmpo 7277	. 2 class (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
33	1, 32	wceq 1539	1 wff Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})

This definition is referenced by:  fullfunc  17622  isfull  17626