Metamath Proof Explorer

Theorem setcco

Description: Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcbas.c 
|- C = ( SetCat ` U )
setcbas.u 
|- ( ph -> U e. V )
setcco.o 
|- .x. = ( comp ` C )
setcco.x 
|- ( ph -> X e. U )
setcco.y 
|- ( ph -> Y e. U )
setcco.z 
|- ( ph -> Z e. U )
setcco.f 
|- ( ph -> F : X --> Y )
setcco.g 
|- ( ph -> G : Y --> Z )
Assertion setcco 
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )

Proof

Step Hyp Ref Expression
1 setcbas.c 
 |-  C = ( SetCat ` U )
2 setcbas.u 
 |-  ( ph -> U e. V )
3 setcco.o 
 |-  .x. = ( comp ` C )
4 setcco.x 
 |-  ( ph -> X e. U )
5 setcco.y 
 |-  ( ph -> Y e. U )
6 setcco.z 
 |-  ( ph -> Z e. U )
7 setcco.f 
 |-  ( ph -> F : X --> Y )
8 setcco.g 
 |-  ( ph -> G : Y --> Z )
9 1 2 3 setccofval 
 |-  ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) )
10 simprr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> z = Z )
11 simprl 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> v = <. X , Y >. )
12 11 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` v ) = ( 2nd ` <. X , Y >. ) )
13 op2ndg 
 |-  ( ( X e. U /\ Y e. U ) -> ( 2nd ` <. X , Y >. ) = Y )
14 4 5 13 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
15 14 adantr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` <. X , Y >. ) = Y )
16 12 15 eqtrd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` v ) = Y )
17 10 16 oveq12d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( z ^m ( 2nd ` v ) ) = ( Z ^m Y ) )
18 11 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 1st ` v ) = ( 1st ` <. X , Y >. ) )
19 op1stg 
 |-  ( ( X e. U /\ Y e. U ) -> ( 1st ` <. X , Y >. ) = X )
20 4 5 19 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
21 20 adantr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 1st ` <. X , Y >. ) = X )
22 18 21 eqtrd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 1st ` v ) = X )
23 16 22 oveq12d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( ( 2nd ` v ) ^m ( 1st ` v ) ) = ( Y ^m X ) )
24 eqidd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( g o. f ) = ( g o. f ) )
25 17 23 24 mpoeq123dv 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) = ( g e. ( Z ^m Y ) , f e. ( Y ^m X ) |-> ( g o. f ) ) )
26 4 5 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( U X. U ) )
27 ovex 
 |-  ( Z ^m Y ) e. _V
28 ovex 
 |-  ( Y ^m X ) e. _V
29 27 28 mpoex 
 |-  ( g e. ( Z ^m Y ) , f e. ( Y ^m X ) |-> ( g o. f ) ) e. _V
30 29 a1i 
 |-  ( ph -> ( g e. ( Z ^m Y ) , f e. ( Y ^m X ) |-> ( g o. f ) ) e. _V )
31 9 25 26 6 30 ovmpod 
 |-  ( ph -> ( <. X , Y >. .x. Z ) = ( g e. ( Z ^m Y ) , f e. ( Y ^m X ) |-> ( g o. f ) ) )
32 simprl 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> g = G )
33 simprr 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> f = F )
34 32 33 coeq12d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( g o. f ) = ( G o. F ) )
35 6 5 elmapd 
 |-  ( ph -> ( G e. ( Z ^m Y ) <-> G : Y --> Z ) )
36 8 35 mpbird 
 |-  ( ph -> G e. ( Z ^m Y ) )
37 5 4 elmapd 
 |-  ( ph -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
38 7 37 mpbird 
 |-  ( ph -> F e. ( Y ^m X ) )
39 coexg 
 |-  ( ( G e. ( Z ^m Y ) /\ F e. ( Y ^m X ) ) -> ( G o. F ) e. _V )
40 36 38 39 syl2anc 
 |-  ( ph -> ( G o. F ) e. _V )
41 31 34 36 38 40 ovmpod 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )