df-coa

Description: Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a quinary operation like the regular composition in a category comp . Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Assertion	df-coa	$⊢ {comp}_{a} = (c \in Cat ⟼ (g \in Arrow (c), f \in \{h \in Arrow (c) \| {cod}_{a} (h) = {dom}_{a} (g)\} ⟼ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (c) {cod}_{a} (g)) 2^{nd} (f)⟩))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccoa	$class {comp}_{a}$
1		vc	$setvar c$
2		ccat	$class Cat$
3		vg	$setvar g$
4		carw	$class Arrow$
5	1	cv	$setvar c$
6	5 4	cfv	$class Arrow (c)$
7		vf	$setvar f$
8		vh	$setvar h$
9		ccoda	$class {cod}_{a}$
10	8	cv	$setvar h$
11	10 9	cfv	$class {cod}_{a} (h)$
12		cdoma	$class {dom}_{a}$
13	3	cv	$setvar g$
14	13 12	cfv	$class {dom}_{a} (g)$
15	11 14	wceq	$wff {cod}_{a} (h) = {dom}_{a} (g)$
16	15 8 6	crab	$class \{h \in Arrow (c) \| {cod}_{a} (h) = {dom}_{a} (g)\}$
17	7	cv	$setvar f$
18	17 12	cfv	$class {dom}_{a} (f)$
19	13 9	cfv	$class {cod}_{a} (g)$
20		c2nd	$class 2^{nd}$
21	13 20	cfv	$class 2^{nd} (g)$
22	18 14	cop	$class ⟨{dom}_{a} (f), {dom}_{a} (g)⟩$
23		cco	$class comp$
24	5 23	cfv	$class comp (c)$
25	22 19 24	co	$class (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (c) {cod}_{a} (g))$
26	17 20	cfv	$class 2^{nd} (f)$
27	21 26 25	co	$class (2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (c) {cod}_{a} (g)) 2^{nd} (f))$
28	18 19 27	cotp	$class ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (c) {cod}_{a} (g)) 2^{nd} (f)⟩$
29	3 7 6 16 28	cmpo	$class (g \in Arrow (c), f \in \{h \in Arrow (c) \| {cod}_{a} (h) = {dom}_{a} (g)\} ⟼ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (c) {cod}_{a} (g)) 2^{nd} (f)⟩)$
30	1 2 29	cmpt	$class (c \in Cat ⟼ (g \in Arrow (c), f \in \{h \in Arrow (c) \| {cod}_{a} (h) = {dom}_{a} (g)\} ⟼ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (c) {cod}_{a} (g)) 2^{nd} (f)⟩))$
31	0 30	wceq	$wff {comp}_{a} = (c \in Cat ⟼ (g \in Arrow (c), f \in \{h \in Arrow (c) \| {cod}_{a} (h) = {dom}_{a} (g)\} ⟼ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (c) {cod}_{a} (g)) 2^{nd} (f)⟩))$

Metamath Proof Explorer

Definition df-coa

Detailed syntax breakdown