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 = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cful 
 |-  Full
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 vd 
 |-  d
4 vf 
 |-  f
5 vg 
 |-  g
6 4 cv 
 |-  f
7 1 cv 
 |-  c
8 cfunc 
 |-  Func
9 3 cv 
 |-  d
10 7 9 8 co 
 |-  ( c Func d )
11 5 cv 
 |-  g
12 6 11 10 wbr 
 |-  f ( c Func d ) g
13 vx 
 |-  x
14 cbs 
 |-  Base
15 7 14 cfv 
 |-  ( Base ` c )
16 vy 
 |-  y
17 13 cv 
 |-  x
18 16 cv 
 |-  y
19 17 18 11 co 
 |-  ( x g y )
20 19 crn 
 |-  ran ( x g y )
21 17 6 cfv 
 |-  ( f ` x )
22 chom 
 |-  Hom
23 9 22 cfv 
 |-  ( Hom ` d )
24 18 6 cfv 
 |-  ( f ` y )
25 21 24 23 co 
 |-  ( ( f ` x ) ( Hom ` d ) ( f ` y ) )
26 20 25 wceq 
 |-  ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) )
27 26 16 15 wral 
 |-  A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) )
28 27 13 15 wral 
 |-  A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) )
29 12 28 wa 
 |-  ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) )
30 29 4 5 copab 
 |-  { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) }
31 1 3 2 2 30 cmpo 
 |-  ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )
32 0 31 wceq 
 |-  Full = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )