coapm

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

	Ref	Expression
Hypotheses	coapm.o	⊢ · = ( comp_a ‘ 𝐶 )
	coapm.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
Assertion	coapm	⊢ · ∈ ( 𝐴 ↑_pm ( 𝐴 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		coapm.o	⊢ · = ( comp_a ‘ 𝐶 )
2		coapm.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
3		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
4	1 2 3	coafval	⊢ · = ( 𝑔 ∈ 𝐴 , 𝑓 ∈ { ℎ ∈ 𝐴 ∣ ( cod_a ‘ ℎ ) = ( dom_a ‘ 𝑔 ) } ↦ ⟨ ( dom_a ‘ 𝑓 ) , ( cod_a ‘ 𝑔 ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( dom_a ‘ 𝑓 ) , ( dom_a ‘ 𝑔 ) ⟩ ( comp ‘ 𝐶 ) ( cod_a ‘ 𝑔 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
5	4	mpofun	⊢ Fun ·
6		funfn	⊢ ( Fun · ↔ · Fn dom · )
7	5 6	mpbi	⊢ · Fn dom ·
8	1 2	dmcoass	⊢ dom · ⊆ ( 𝐴 × 𝐴 )
9	8	sseli	⊢ ( 𝑧 ∈ dom · → 𝑧 ∈ ( 𝐴 × 𝐴 ) )
10		1st2nd2	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐴 ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
11	9 10	syl	⊢ ( 𝑧 ∈ dom · → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
12	11	fveq2d	⊢ ( 𝑧 ∈ dom · → ( · ‘ 𝑧 ) = ( · ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
13		df-ov	⊢ ( ( 1^st ‘ 𝑧 ) · ( 2^nd ‘ 𝑧 ) ) = ( · ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
14	12 13	eqtr4di	⊢ ( 𝑧 ∈ dom · → ( · ‘ 𝑧 ) = ( ( 1^st ‘ 𝑧 ) · ( 2^nd ‘ 𝑧 ) ) )
15		eqid	⊢ ( Hom_a ‘ 𝐶 ) = ( Hom_a ‘ 𝐶 )
16	2 15	homarw	⊢ ( ( dom_a ‘ ( 2^nd ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( cod_a ‘ ( 1^st ‘ 𝑧 ) ) ) ⊆ 𝐴
17		id	⊢ ( 𝑧 ∈ dom · → 𝑧 ∈ dom · )
18	11 17	eqeltrrd	⊢ ( 𝑧 ∈ dom · → ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∈ dom · )
19		df-br	⊢ ( ( 1^st ‘ 𝑧 ) dom · ( 2^nd ‘ 𝑧 ) ↔ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∈ dom · )
20	18 19	sylibr	⊢ ( 𝑧 ∈ dom · → ( 1^st ‘ 𝑧 ) dom · ( 2^nd ‘ 𝑧 ) )
21	1 2	eldmcoa	⊢ ( ( 1^st ‘ 𝑧 ) dom · ( 2^nd ‘ 𝑧 ) ↔ ( ( 2^nd ‘ 𝑧 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( cod_a ‘ ( 2^nd ‘ 𝑧 ) ) = ( dom_a ‘ ( 1^st ‘ 𝑧 ) ) ) )
22	20 21	sylib	⊢ ( 𝑧 ∈ dom · → ( ( 2^nd ‘ 𝑧 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( cod_a ‘ ( 2^nd ‘ 𝑧 ) ) = ( dom_a ‘ ( 1^st ‘ 𝑧 ) ) ) )
23	22	simp1d	⊢ ( 𝑧 ∈ dom · → ( 2^nd ‘ 𝑧 ) ∈ 𝐴 )
24	2 15	arwhoma	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ 𝐴 → ( 2^nd ‘ 𝑧 ) ∈ ( ( dom_a ‘ ( 2^nd ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( cod_a ‘ ( 2^nd ‘ 𝑧 ) ) ) )
25	23 24	syl	⊢ ( 𝑧 ∈ dom · → ( 2^nd ‘ 𝑧 ) ∈ ( ( dom_a ‘ ( 2^nd ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( cod_a ‘ ( 2^nd ‘ 𝑧 ) ) ) )
26	22	simp3d	⊢ ( 𝑧 ∈ dom · → ( cod_a ‘ ( 2^nd ‘ 𝑧 ) ) = ( dom_a ‘ ( 1^st ‘ 𝑧 ) ) )
27	26	oveq2d	⊢ ( 𝑧 ∈ dom · → ( ( dom_a ‘ ( 2^nd ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( cod_a ‘ ( 2^nd ‘ 𝑧 ) ) ) = ( ( dom_a ‘ ( 2^nd ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( dom_a ‘ ( 1^st ‘ 𝑧 ) ) ) )
28	25 27	eleqtrd	⊢ ( 𝑧 ∈ dom · → ( 2^nd ‘ 𝑧 ) ∈ ( ( dom_a ‘ ( 2^nd ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( dom_a ‘ ( 1^st ‘ 𝑧 ) ) ) )
29	22	simp2d	⊢ ( 𝑧 ∈ dom · → ( 1^st ‘ 𝑧 ) ∈ 𝐴 )
30	2 15	arwhoma	⊢ ( ( 1^st ‘ 𝑧 ) ∈ 𝐴 → ( 1^st ‘ 𝑧 ) ∈ ( ( dom_a ‘ ( 1^st ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( cod_a ‘ ( 1^st ‘ 𝑧 ) ) ) )
31	29 30	syl	⊢ ( 𝑧 ∈ dom · → ( 1^st ‘ 𝑧 ) ∈ ( ( dom_a ‘ ( 1^st ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( cod_a ‘ ( 1^st ‘ 𝑧 ) ) ) )
32	1 15 28 31	coahom	⊢ ( 𝑧 ∈ dom · → ( ( 1^st ‘ 𝑧 ) · ( 2^nd ‘ 𝑧 ) ) ∈ ( ( dom_a ‘ ( 2^nd ‘ 𝑧 ) ) ( Hom_a ‘ 𝐶 ) ( cod_a ‘ ( 1^st ‘ 𝑧 ) ) ) )
33	16 32	sseldi	⊢ ( 𝑧 ∈ dom · → ( ( 1^st ‘ 𝑧 ) · ( 2^nd ‘ 𝑧 ) ) ∈ 𝐴 )
34	14 33	eqeltrd	⊢ ( 𝑧 ∈ dom · → ( · ‘ 𝑧 ) ∈ 𝐴 )
35	34	rgen	⊢ ∀ 𝑧 ∈ dom · ( · ‘ 𝑧 ) ∈ 𝐴
36		ffnfv	⊢ ( · : dom · ⟶ 𝐴 ↔ ( · Fn dom · ∧ ∀ 𝑧 ∈ dom · ( · ‘ 𝑧 ) ∈ 𝐴 ) )
37	7 35 36	mpbir2an	⊢ · : dom · ⟶ 𝐴
38	2	fvexi	⊢ 𝐴 ∈ V
39	38 38	xpex	⊢ ( 𝐴 × 𝐴 ) ∈ V
40	38 39	elpm2	⊢ ( · ∈ ( 𝐴 ↑_pm ( 𝐴 × 𝐴 ) ) ↔ ( · : dom · ⟶ 𝐴 ∧ dom · ⊆ ( 𝐴 × 𝐴 ) ) )
41	37 8 40	mpbir2an	⊢ · ∈ ( 𝐴 ↑_pm ( 𝐴 × 𝐴 ) )

Metamath Proof Explorer

Theorem coapm

Proof