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 \in Cat, d \in Cat ⟼ \{⟨f, g⟩ \| (f (c Func d) g \land \forall x \in {Base}_{c} \forall y \in {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 \forall y \in {Base}_{c} Fun {(x g y)}^{-1}$
23	22 13 15	wral	$wff \forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1}$
24	12 23	wa	$wff (f (c Func d) g \land \forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1})$
25	24 4 5	copab	$class \{⟨f, g⟩ \| (f (c Func d) g \land \forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1})\}$
26	1 3 2 2 25	cmpo	$class (c \in Cat, d \in Cat ⟼ \{⟨f, g⟩ \| (f (c Func d) g \land \forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1})\})$
27	0 26	wceq	$wff Faith = (c \in Cat, d \in Cat ⟼ \{⟨f, g⟩ \| (f (c Func d) g \land \forall x \in {Base}_{c} \forall y \in {Base}_{c} Fun {(x g y)}^{-1})\})$

Metamath Proof Explorer

Definition df-fth

Detailed syntax breakdown