Metamath Proof Explorer

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 ⊢ Full = c ∈ Cat , d ∈ Cat ⟼ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c ran ⁡ x g y = f ⁡ x Hom ⁡ d f ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cful class Full
1 vc setvar c
2 ccat class Cat
3 vd setvar d
4 vf setvar f
5 vg setvar g
6 4 cv setvar f
7 1 cv setvar c
8 cfunc class Func
9 3 cv setvar d
10 7 9 8 co class c Func d
11 5 cv setvar g
12 6 11 10 wbr wff f c Func d g
13 vx setvar x
14 cbs class Base
15 7 14 cfv class Base c
16 vy setvar y
17 13 cv setvar x
18 16 cv setvar y
19 17 18 11 co class x g y
20 19 crn class ran ⁡ x g y
21 17 6 cfv class f ⁡ x
22 chom class Hom
23 9 22 cfv class Hom ⁡ d
24 18 6 cfv class f ⁡ y
25 21 24 23 co class f ⁡ x Hom ⁡ d f ⁡ y
26 20 25 wceq wff ran ⁡ x g y = f ⁡ x Hom ⁡ d f ⁡ y
27 26 16 15 wral wff ∀ y ∈ Base c ran ⁡ x g y = f ⁡ x Hom ⁡ d f ⁡ y
28 27 13 15 wral wff ∀ x ∈ Base c ∀ y ∈ Base c ran ⁡ x g y = f ⁡ x Hom ⁡ d f ⁡ y
29 12 28 wa wff f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c ran ⁡ x g y = f ⁡ x Hom ⁡ d f ⁡ y
30 29 4 5 copab class f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c ran ⁡ x g y = f ⁡ x Hom ⁡ d f ⁡ y
31 1 3 2 2 30 cmpo class c ∈ Cat , d ∈ Cat ⟼ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c ran ⁡ x g y = f ⁡ x Hom ⁡ d f ⁡ y
32 0 31 wceq wff Full = c ∈ Cat , d ∈ Cat ⟼ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c ran ⁡ x g y = f ⁡ x Hom ⁡ d f ⁡ y