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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cful	⊢ Full
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	crn	⊢ ran ( 𝑥 𝑔 𝑦 )
21	17 6	cfv	⊢ ( 𝑓 ‘ 𝑥 )
22		chom	⊢ Hom
23	9 22	cfv	⊢ ( Hom ‘ 𝑑 )
24	18 6	cfv	⊢ ( 𝑓 ‘ 𝑦 )
25	21 24 23	co	⊢ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) )
26	20 25	wceq	⊢ ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) )
27	26 16 15	wral	⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) )
28	27 13 15	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) )
29	12 28	wa	⊢ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) )
30	29 4 5	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) }
31	1 3 2 2 30	cmpo	⊢ ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
32	0 31	wceq	⊢ Full = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } )