Metamath Proof Explorer

Theorem catcco

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

Ref Expression
Hypotheses catcbas.c 
|- C = ( CatCat ` U )
catcbas.b 
|- B = ( Base ` C )
catcbas.u 
|- ( ph -> U e. V )
catcco.o 
|- .x. = ( comp ` C )
catcco.x 
|- ( ph -> X e. B )
catcco.y 
|- ( ph -> Y e. B )
catcco.z 
|- ( ph -> Z e. B )
catcco.f 
|- ( ph -> F e. ( X Func Y ) )
catcco.g 
|- ( ph -> G e. ( Y Func Z ) )
Assertion catcco 
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o.func F ) )

Proof

Step Hyp Ref Expression
1 catcbas.c 
 |-  C = ( CatCat ` U )
2 catcbas.b 
 |-  B = ( Base ` C )
3 catcbas.u 
 |-  ( ph -> U e. V )
4 catcco.o 
 |-  .x. = ( comp ` C )
5 catcco.x 
 |-  ( ph -> X e. B )
6 catcco.y 
 |-  ( ph -> Y e. B )
7 catcco.z 
 |-  ( ph -> Z e. B )
8 catcco.f 
 |-  ( ph -> F e. ( X Func Y ) )
9 catcco.g 
 |-  ( ph -> G e. ( Y Func Z ) )
10 1 2 3 4 catccofval 
 |-  ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) ) )
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. B /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
14 5 6 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 simprr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> z = Z )
18 16 17 oveq12d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( ( 2nd ` v ) Func z ) = ( Y Func Z ) )
19 11 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( Func ` v ) = ( Func ` <. X , Y >. ) )
20 df-ov 
 |-  ( X Func Y ) = ( Func ` <. X , Y >. )
21 19 20 eqtr4di 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( Func ` v ) = ( X Func Y ) )
22 eqidd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( g o.func f ) = ( g o.func f ) )
23 18 21 22 mpoeq123dv 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( g e. ( ( 2nd ` v ) Func z ) , f e. ( Func ` v ) |-> ( g o.func f ) ) = ( g e. ( Y Func Z ) , f e. ( X Func Y ) |-> ( g o.func f ) ) )
24 5 6 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
25 ovex 
 |-  ( Y Func Z ) e. _V
26 ovex 
 |-  ( X Func Y ) e. _V
27 25 26 mpoex 
 |-  ( g e. ( Y Func Z ) , f e. ( X Func Y ) |-> ( g o.func f ) ) e. _V
28 27 a1i 
 |-  ( ph -> ( g e. ( Y Func Z ) , f e. ( X Func Y ) |-> ( g o.func f ) ) e. _V )
29 10 23 24 7 28 ovmpod 
 |-  ( ph -> ( <. X , Y >. .x. Z ) = ( g e. ( Y Func Z ) , f e. ( X Func Y ) |-> ( g o.func f ) ) )
30 oveq12 
 |-  ( ( g = G /\ f = F ) -> ( g o.func f ) = ( G o.func F ) )
31 30 adantl 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( g o.func f ) = ( G o.func F ) )
32 ovexd 
 |-  ( ph -> ( G o.func F ) e. _V )
33 29 31 9 8 32 ovmpod 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o.func F ) )