coapm

Description: Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	coapm.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
	coapm.a	$⊢ A = Arrow (C)$
Assertion	coapm	$⊢ \underset{˙}{\cdot} \in (A ↑_{𝑝𝑚} (A \times A))$

Proof

Step	Hyp	Ref	Expression
1		coapm.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
2		coapm.a	$⊢ A = Arrow (C)$
3		eqid	$⊢ comp (C) = comp (C)$
4	1 2 3	coafval	$⊢ \underset{˙}{\cdot} = (g \in A, f \in \{h \in A \| {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)⟩)$
5	4	mpofun	$⊢ Fun \underset{˙}{\cdot}$
6		funfn	$⊢ Fun \underset{˙}{\cdot} \leftrightarrow \underset{˙}{\cdot} Fn dom \underset{˙}{\cdot}$
7	5 6	mpbi	$⊢ \underset{˙}{\cdot} Fn dom \underset{˙}{\cdot}$
8	1 2	dmcoass	$⊢ dom \underset{˙}{\cdot} \subseteq A \times A$
9	8	sseli	$⊢ z \in dom \underset{˙}{\cdot} \to z \in (A \times A)$
10		1st2nd2	$⊢ z \in (A \times A) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
11	9 10	syl	$⊢ z \in dom \underset{˙}{\cdot} \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
12	11	fveq2d	$⊢ z \in dom \underset{˙}{\cdot} \to \underset{˙}{\cdot} (z) = \underset{˙}{\cdot} (⟨1^{st} (z), 2^{nd} (z)⟩)$
13		df-ov	$⊢ 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (z) = \underset{˙}{\cdot} (⟨1^{st} (z), 2^{nd} (z)⟩)$
14	12 13	eqtr4di	$⊢ z \in dom \underset{˙}{\cdot} \to \underset{˙}{\cdot} (z) = 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (z)$
15		eqid	$⊢ {Hom}_{a} (C) = {Hom}_{a} (C)$
16	2 15	homarw	$⊢ {dom}_{a} (2^{nd} (z)) {Hom}_{a} (C) {cod}_{a} (1^{st} (z)) \subseteq A$
17		id	$⊢ z \in dom \underset{˙}{\cdot} \to z \in dom \underset{˙}{\cdot}$
18	11 17	eqeltrrd	$⊢ z \in dom \underset{˙}{\cdot} \to ⟨1^{st} (z), 2^{nd} (z)⟩ \in dom \underset{˙}{\cdot}$
19		df-br	$⊢ 1^{st} (z) dom \underset{˙}{\cdot} 2^{nd} (z) \leftrightarrow ⟨1^{st} (z), 2^{nd} (z)⟩ \in dom \underset{˙}{\cdot}$
20	18 19	sylibr	$⊢ z \in dom \underset{˙}{\cdot} \to 1^{st} (z) dom \underset{˙}{\cdot} 2^{nd} (z)$
21	1 2	eldmcoa	$⊢ 1^{st} (z) dom \underset{˙}{\cdot} 2^{nd} (z) \leftrightarrow (2^{nd} (z) \in A \land 1^{st} (z) \in A \land {cod}_{a} (2^{nd} (z)) = {dom}_{a} (1^{st} (z)))$
22	20 21	sylib	$⊢ z \in dom \underset{˙}{\cdot} \to (2^{nd} (z) \in A \land 1^{st} (z) \in A \land {cod}_{a} (2^{nd} (z)) = {dom}_{a} (1^{st} (z)))$
23	22	simp1d	$⊢ z \in dom \underset{˙}{\cdot} \to 2^{nd} (z) \in A$
24	2 15	arwhoma	$⊢ 2^{nd} (z) \in A \to 2^{nd} (z) \in ({dom}_{a} (2^{nd} (z)) {Hom}_{a} (C) {cod}_{a} (2^{nd} (z)))$
25	23 24	syl	$⊢ z \in dom \underset{˙}{\cdot} \to 2^{nd} (z) \in ({dom}_{a} (2^{nd} (z)) {Hom}_{a} (C) {cod}_{a} (2^{nd} (z)))$
26	22	simp3d	$⊢ z \in dom \underset{˙}{\cdot} \to {cod}_{a} (2^{nd} (z)) = {dom}_{a} (1^{st} (z))$
27	26	oveq2d	$⊢ z \in dom \underset{˙}{\cdot} \to {dom}_{a} (2^{nd} (z)) {Hom}_{a} (C) {cod}_{a} (2^{nd} (z)) = {dom}_{a} (2^{nd} (z)) {Hom}_{a} (C) {dom}_{a} (1^{st} (z))$
28	25 27	eleqtrd	$⊢ z \in dom \underset{˙}{\cdot} \to 2^{nd} (z) \in ({dom}_{a} (2^{nd} (z)) {Hom}_{a} (C) {dom}_{a} (1^{st} (z)))$
29	22	simp2d	$⊢ z \in dom \underset{˙}{\cdot} \to 1^{st} (z) \in A$
30	2 15	arwhoma	$⊢ 1^{st} (z) \in A \to 1^{st} (z) \in ({dom}_{a} (1^{st} (z)) {Hom}_{a} (C) {cod}_{a} (1^{st} (z)))$
31	29 30	syl	$⊢ z \in dom \underset{˙}{\cdot} \to 1^{st} (z) \in ({dom}_{a} (1^{st} (z)) {Hom}_{a} (C) {cod}_{a} (1^{st} (z)))$
32	1 15 28 31	coahom	$⊢ z \in dom \underset{˙}{\cdot} \to 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (z) \in ({dom}_{a} (2^{nd} (z)) {Hom}_{a} (C) {cod}_{a} (1^{st} (z)))$
33	16 32	sselid	$⊢ z \in dom \underset{˙}{\cdot} \to 1^{st} (z) \underset{˙}{\cdot} 2^{nd} (z) \in A$
34	14 33	eqeltrd	$⊢ z \in dom \underset{˙}{\cdot} \to \underset{˙}{\cdot} (z) \in A$
35	34	rgen	$⊢ \forall z \in dom \underset{˙}{\cdot} \underset{˙}{\cdot} (z) \in A$
36		ffnfv	$⊢ \underset{˙}{\cdot} : dom \underset{˙}{\cdot} ⟶ A \leftrightarrow (\underset{˙}{\cdot} Fn dom \underset{˙}{\cdot} \land \forall z \in dom \underset{˙}{\cdot} \underset{˙}{\cdot} (z) \in A)$
37	7 35 36	mpbir2an	$⊢ \underset{˙}{\cdot} : dom \underset{˙}{\cdot} ⟶ A$
38	2	fvexi	$⊢ A \in V$
39	38 38	xpex	$⊢ A \times A \in V$
40	38 39	elpm2	$⊢ \underset{˙}{\cdot} \in (A ↑_{𝑝𝑚} (A \times A)) \leftrightarrow (\underset{˙}{\cdot} : dom \underset{˙}{\cdot} ⟶ A \land dom \underset{˙}{\cdot} \subseteq A \times A)$
41	37 8 40	mpbir2an	$⊢ \underset{˙}{\cdot} \in (A ↑_{𝑝𝑚} (A \times A))$

Metamath Proof Explorer

Theorem coapm

Proof