This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } )