Metamath Proof Explorer

Theorem coapm

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

Ref Expression
Hypotheses coapm.o 
|- .x. = ( compA ` C )
coapm.a 
|- A = ( Arrow ` C )
Assertion coapm 
|- .x. e. ( A ^pm ( A X. A ) )

Proof

Step Hyp Ref Expression
1 coapm.o 
 |-  .x. = ( compA ` C )
2 coapm.a 
 |-  A = ( Arrow ` C )
3 eqid 
 |-  ( comp ` C ) = ( comp ` C )
4 1 2 3 coafval 
 |-  .x. = ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` C ) ( codA ` g ) ) ( 2nd ` f ) ) >. )
5 4 mpofun 
 |-  Fun .x.
6 funfn 
 |-  ( Fun .x. <-> .x. Fn dom .x. )
7 5 6 mpbi 
 |-  .x. Fn dom .x.
8 1 2 dmcoass 
 |-  dom .x. C_ ( A X. A )
9 8 sseli 
 |-  ( z e. dom .x. -> z e. ( A X. A ) )
10 1st2nd2 
 |-  ( z e. ( A X. A ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
11 9 10 syl 
 |-  ( z e. dom .x. -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
12 11 fveq2d 
 |-  ( z e. dom .x. -> ( .x. ` z ) = ( .x. ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
13 df-ov 
 |-  ( ( 1st ` z ) .x. ( 2nd ` z ) ) = ( .x. ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
14 12 13 eqtr4di 
 |-  ( z e. dom .x. -> ( .x. ` z ) = ( ( 1st ` z ) .x. ( 2nd ` z ) ) )
15 eqid 
 |-  ( HomA ` C ) = ( HomA ` C )
16 2 15 homarw 
 |-  ( ( domA ` ( 2nd ` z ) ) ( HomA ` C ) ( codA ` ( 1st ` z ) ) ) C_ A
17 id 
 |-  ( z e. dom .x. -> z e. dom .x. )
18 11 17 eqeltrrd 
 |-  ( z e. dom .x. -> <. ( 1st ` z ) , ( 2nd ` z ) >. e. dom .x. )
19 df-br 
 |-  ( ( 1st ` z ) dom .x. ( 2nd ` z ) <-> <. ( 1st ` z ) , ( 2nd ` z ) >. e. dom .x. )
20 18 19 sylibr 
 |-  ( z e. dom .x. -> ( 1st ` z ) dom .x. ( 2nd ` z ) )
21 1 2 eldmcoa 
 |-  ( ( 1st ` z ) dom .x. ( 2nd ` z ) <-> ( ( 2nd ` z ) e. A /\ ( 1st ` z ) e. A /\ ( codA ` ( 2nd ` z ) ) = ( domA ` ( 1st ` z ) ) ) )
22 20 21 sylib 
 |-  ( z e. dom .x. -> ( ( 2nd ` z ) e. A /\ ( 1st ` z ) e. A /\ ( codA ` ( 2nd ` z ) ) = ( domA ` ( 1st ` z ) ) ) )
23 22 simp1d 
 |-  ( z e. dom .x. -> ( 2nd ` z ) e. A )
24 2 15 arwhoma 
 |-  ( ( 2nd ` z ) e. A -> ( 2nd ` z ) e. ( ( domA ` ( 2nd ` z ) ) ( HomA ` C ) ( codA ` ( 2nd ` z ) ) ) )
25 23 24 syl 
 |-  ( z e. dom .x. -> ( 2nd ` z ) e. ( ( domA ` ( 2nd ` z ) ) ( HomA ` C ) ( codA ` ( 2nd ` z ) ) ) )
26 22 simp3d 
 |-  ( z e. dom .x. -> ( codA ` ( 2nd ` z ) ) = ( domA ` ( 1st ` z ) ) )
27 26 oveq2d 
 |-  ( z e. dom .x. -> ( ( domA ` ( 2nd ` z ) ) ( HomA ` C ) ( codA ` ( 2nd ` z ) ) ) = ( ( domA ` ( 2nd ` z ) ) ( HomA ` C ) ( domA ` ( 1st ` z ) ) ) )
28 25 27 eleqtrd 
 |-  ( z e. dom .x. -> ( 2nd ` z ) e. ( ( domA ` ( 2nd ` z ) ) ( HomA ` C ) ( domA ` ( 1st ` z ) ) ) )
29 22 simp2d 
 |-  ( z e. dom .x. -> ( 1st ` z ) e. A )
30 2 15 arwhoma 
 |-  ( ( 1st ` z ) e. A -> ( 1st ` z ) e. ( ( domA ` ( 1st ` z ) ) ( HomA ` C ) ( codA ` ( 1st ` z ) ) ) )
31 29 30 syl 
 |-  ( z e. dom .x. -> ( 1st ` z ) e. ( ( domA ` ( 1st ` z ) ) ( HomA ` C ) ( codA ` ( 1st ` z ) ) ) )
32 1 15 28 31 coahom 
 |-  ( z e. dom .x. -> ( ( 1st ` z ) .x. ( 2nd ` z ) ) e. ( ( domA ` ( 2nd ` z ) ) ( HomA ` C ) ( codA ` ( 1st ` z ) ) ) )
33 16 32 sselid 
 |-  ( z e. dom .x. -> ( ( 1st ` z ) .x. ( 2nd ` z ) ) e. A )
34 14 33 eqeltrd 
 |-  ( z e. dom .x. -> ( .x. ` z ) e. A )
35 34 rgen 
 |-  A. z e. dom .x. ( .x. ` z ) e. A
36 ffnfv 
 |-  ( .x. : dom .x. --> A <-> ( .x. Fn dom .x. /\ A. z e. dom .x. ( .x. ` z ) e. A ) )
37 7 35 36 mpbir2an 
 |-  .x. : dom .x. --> A
38 2 fvexi 
 |-  A e. _V
39 38 38 xpex 
 |-  ( A X. A ) e. _V
40 38 39 elpm2 
 |-  ( .x. e. ( A ^pm ( A X. A ) ) <-> ( .x. : dom .x. --> A /\ dom .x. C_ ( A X. A ) ) )
41 37 8 40 mpbir2an 
 |-  .x. e. ( A ^pm ( A X. A ) )