# 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 ${⊢}\mathrm{Faith}=\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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{\left({x}{g}{y}\right)}^{-1}\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cfth ${class}\mathrm{Faith}$
1 vc ${setvar}{c}$
2 ccat ${class}\mathrm{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}\mathrm{Func}$
9 3 cv ${setvar}{d}$
10 7 9 8 co ${class}\left({c}\mathrm{Func}{d}\right)$
11 5 cv ${setvar}{g}$
12 6 11 10 wbr ${wff}{f}\left({c}\mathrm{Func}{d}\right){g}$
13 vx ${setvar}{x}$
14 cbs ${class}\mathrm{Base}$
15 7 14 cfv ${class}{\mathrm{Base}}_{{c}}$
16 vy ${setvar}{y}$
17 13 cv ${setvar}{x}$
18 16 cv ${setvar}{y}$
19 17 18 11 co ${class}\left({x}{g}{y}\right)$
20 19 ccnv ${class}{\left({x}{g}{y}\right)}^{-1}$
21 20 wfun ${wff}\mathrm{Fun}{\left({x}{g}{y}\right)}^{-1}$
22 21 16 15 wral ${wff}\forall {y}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{\left({x}{g}{y}\right)}^{-1}$
23 22 13 15 wral ${wff}\forall {x}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{\left({x}{g}{y}\right)}^{-1}$
24 12 23 wa ${wff}\left({f}\left({c}\mathrm{Func}{d}\right){g}\wedge \forall {x}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{\left({x}{g}{y}\right)}^{-1}\right)$
25 24 4 5 copab ${class}\left\{⟨{f},{g}⟩|\left({f}\left({c}\mathrm{Func}{d}\right){g}\wedge \forall {x}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{\left({x}{g}{y}\right)}^{-1}\right)\right\}$
26 1 3 2 2 25 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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{\left({x}{g}{y}\right)}^{-1}\right)\right\}\right)$
27 0 26 wceq ${wff}\mathrm{Faith}=\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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{\left({x}{g}{y}\right)}^{-1}\right)\right\}\right)$