Definition df-mon 16390

Description: Function returning the monomorphisms of the category c. JFM CAT₁ def. 10. (Contributed by FL, 5-Dec-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
df-mon	|- Mono = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) ) } ) )

Distinct variable group:   b, c, f, g, h, x, y, z

Detailed syntax breakdown of Definition df-mon

Step	Hyp	Ref	Expression
1		cmon 16388	. 2 class Mono
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . 5 class c
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` c )
8		vh	. . . . 5 setvar h
9		chom 15952	. . . . . 6 class Hom
10	5, 9	cfv 5888	. . . . 5 class ( Hom ` c )
11		vx	. . . . . 6 setvar x
12		vy	. . . . . 6 setvar y
13	4	cv 1482	. . . . . 6 class b
14		vg	. . . . . . . . . . 11 setvar g
15		vz	. . . . . . . . . . . . 13 setvar z
16	15	cv 1482	. . . . . . . . . . . 12 class z
17	11	cv 1482	. . . . . . . . . . . 12 class x
18	8	cv 1482	. . . . . . . . . . . 12 class h
19	16, 17, 18	co 6650	. . . . . . . . . . 11 class ( z h x )
20		vf	. . . . . . . . . . . . 13 setvar f
21	20	cv 1482	. . . . . . . . . . . 12 class f
22	14	cv 1482	. . . . . . . . . . . 12 class g
23	16, 17	cop 4183	. . . . . . . . . . . . 13 class <. z , x >.
24	12	cv 1482	. . . . . . . . . . . . 13 class y
25		cco 15953	. . . . . . . . . . . . . 14 class comp
26	5, 25	cfv 5888	. . . . . . . . . . . . 13 class (comp ` c )
27	23, 24, 26	co 6650	. . . . . . . . . . . 12 class ( <. z , x >. (comp ` c ) y )
28	21, 22, 27	co 6650	. . . . . . . . . . 11 class ( f ( <. z , x >. (comp ` c ) y ) g )
29	14, 19, 28	cmpt 4729	. . . . . . . . . 10 class ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) )
30	29	ccnv 5113	. . . . . . . . 9 class `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) )
31	30	wfun 5882	. . . . . . . 8 wff Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) )
32	31, 15, 13	wral 2912	. . . . . . 7 wff A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) )
33	17, 24, 18	co 6650	. . . . . . 7 class ( x h y )
34	32, 20, 33	crab 2916	. . . . . 6 class { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) ) }
35	11, 12, 13, 13, 34	cmpt2 6652	. . . . 5 class ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) ) } )
36	8, 10, 35	csb 3533	. . . 4 class [_ ( Hom ` c ) / h ]_ ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) ) } )
37	4, 7, 36	csb 3533	. . 3 class [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) ) } )
38	2, 3, 37	cmpt 4729	. 2 class ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) ) } ) )
39	1, 38	wceq 1483	1 wff Mono = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. (comp ` c ) y ) g ) ) } ) )

This definition is referenced by:  monfval  16392