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 = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfth	⊢ Faith
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		vd	⊢ 𝑑
4		vf	⊢ 𝑓
5		vg	⊢ 𝑔
6	4	cv	⊢ 𝑓
7	1	cv	⊢ 𝑐
8		cfunc	⊢ Func
9	3	cv	⊢ 𝑑
10	7 9 8	co	⊢ ( 𝑐 Func 𝑑 )
11	5	cv	⊢ 𝑔
12	6 11 10	wbr	⊢ 𝑓 ( 𝑐 Func 𝑑 ) 𝑔
13		vx	⊢ 𝑥
14		cbs	⊢ Base
15	7 14	cfv	⊢ ( Base ‘ 𝑐 )
16		vy	⊢ 𝑦
17	13	cv	⊢ 𝑥
18	16	cv	⊢ 𝑦
19	17 18 11	co	⊢ ( 𝑥 𝑔 𝑦 )
20	19	ccnv	⊢ ◡ ( 𝑥 𝑔 𝑦 )
21	20	wfun	⊢ Fun ◡ ( 𝑥 𝑔 𝑦 )
22	21 16 15	wral	⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 )
23	22 13 15	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 )
24	12 23	wa	⊢ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) )
25	24 4 5	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) }
26	1 3 2 2 25	cmpo	⊢ ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
27	0 26	wceq	⊢ Faith = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )