Definition df-hom 10665

Description: (hom` x) is a function which returns for each pair of objects <.a, b>. the morphisms whose domain is a and codomain b. JFM CAT₁ def. 6

Assertion

Ref	Expression
df-hom	|- hom = {<.x, y>. | (x e. Cat /\ y = {<.<.a, b>., c>. | (a e. dom (id` x) /\ b e. dom (id` x) /\ c = {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)})})}

Distinct variable group:   x,y,a,b,c,f

Detailed syntax breakdown of Definition df-hom

Step	Hyp	Ref	Expression
1		chom 10664	. 2 class hom
2		vx	. . . . . 6 set x
3	2	cv 954	. . . . 5 class x
4		ccat 10636	. . . . 5 class Cat
5	3, 4	wcel 957	. . . 4 wff x e. Cat
6		vy	. . . . . 6 set y
7	6	cv 954	. . . . 5 class y
8		va	. . . . . . . . 9 set a
9	8	cv 954	. . . . . . . 8 class a
10		cid_ 10597	. . . . . . . . . 10 class id
11	3, 10	cfv 3179	. . . . . . . . 9 class (id` x)
12	11	cdm 3167	. . . . . . . 8 class dom (id` x)
13	9, 12	wcel 957	. . . . . . 7 wff a e. dom (id` x)
14		vb	. . . . . . . . 9 set b
15	14	cv 954	. . . . . . . 8 class b
16	15, 12	wcel 957	. . . . . . 7 wff b e. dom (id` x)
17		vc	. . . . . . . . 9 set c
18	17	cv 954	. . . . . . . 8 class c
19		vf	. . . . . . . . . . . 12 set f
20	19	cv 954	. . . . . . . . . . 11 class f
21		cdom_ 10595	. . . . . . . . . . . . 13 class dom
22	3, 21	cfv 3179	. . . . . . . . . . . 12 class (dom` x)
23	22	cdm 3167	. . . . . . . . . . 11 class dom (dom` x)
24	20, 23	wcel 957	. . . . . . . . . 10 wff f e. dom (dom` x)
25	20, 22	cfv 3179	. . . . . . . . . . 11 class ((dom` x)` f)
26	25, 9	wceq 955	. . . . . . . . . 10 wff ((dom` x)` f) = a
27		ccod_ 10596	. . . . . . . . . . . . 13 class cod
28	3, 27	cfv 3179	. . . . . . . . . . . 12 class (cod` x)
29	20, 28	cfv 3179	. . . . . . . . . . 11 class ((cod` x)` f)
30	29, 15	wceq 955	. . . . . . . . . 10 wff ((cod` x)` f) = b
31	24, 26, 30	w3a 774	. . . . . . . . 9 wff (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)
32	31, 19	cab 1463	. . . . . . . 8 class {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)}
33	18, 32	wceq 955	. . . . . . 7 wff c = {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)}
34	13, 16, 33	w3a 774	. . . . . 6 wff (a e. dom (id` x) /\ b e. dom (id` x) /\ c = {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)})
35	34, 8, 14, 17	copab2 3961	. . . . 5 class {<.<.a, b>., c>. | (a e. dom (id` x) /\ b e. dom (id` x) /\ c = {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)})}
36	7, 35	wceq 955	. . . 4 wff y = {<.<.a, b>., c>. | (a e. dom (id` x) /\ b e. dom (id` x) /\ c = {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)})}
37	5, 36	wa 223	. . 3 wff (x e. Cat /\ y = {<.<.a, b>., c>. | (a e. dom (id` x) /\ b e. dom (id` x) /\ c = {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)})})
38	37, 2, 6	copab 2663	. 2 class {<.x, y>. | (x e. Cat /\ y = {<.<.a, b>., c>. | (a e. dom (id` x) /\ b e. dom (id` x) /\ c = {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)})})}
39	1, 38	wceq 955	1 wff hom = {<.x, y>. | (x e. Cat /\ y = {<.<.a, b>., c>. | (a e. dom (id` x) /\ b e. dom (id` x) /\ c = {f | (f e. dom (dom` x) /\ ((dom` x)` f) = a /\ ((cod` x)` f) = b)})})}

This definition is referenced by:  ishoma 10666

Copyright terms: Public domain