Metamath Proof Explorer

Definition df-fth

Description: Function returning all the faithful functors from a category C to a category D . A faithful functor is a functor in which all the morphism maps G ( X , Y ) between objects X , Y e. C are injections. Definition 3.27(2) in Adamek p. 34. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Assertion df-fth ⊢ Faith = c ∈ Cat , d ∈ Cat ⟼ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfth class Faith
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 ccnv class x g y -1
21 20 wfun wff Fun ⁡ x g y -1
22 21 16 15 wral wff ∀ y ∈ Base c Fun ⁡ x g y -1
23 22 13 15 wral wff ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1
24 12 23 wa wff f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1
25 24 4 5 copab class f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1
26 1 3 2 2 25 cmpo class c ∈ Cat , d ∈ Cat ⟼ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1
27 0 26 wceq wff Faith = c ∈ Cat , d ∈ Cat ⟼ f g | f c Func d g ∧ ∀ x ∈ Base c ∀ y ∈ Base c Fun ⁡ x g y -1