MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fucpropd Unicode version

Theorem fucpropd 14129
Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same functor categories. (Contributed by Mario Carneiro, 26-Jan-2017.)
Hypotheses
Ref Expression
fucpropd.1  |-  ( ph  ->  (  Homf 
`  A )  =  (  Homf 
`  B ) )
fucpropd.2  |-  ( ph  ->  (compf `  A )  =  (compf `  B ) )
fucpropd.3  |-  ( ph  ->  (  Homf 
`  C )  =  (  Homf 
`  D ) )
fucpropd.4  |-  ( ph  ->  (compf `  C )  =  (compf `  D ) )
fucpropd.a  |-  ( ph  ->  A  e.  Cat )
fucpropd.b  |-  ( ph  ->  B  e.  Cat )
fucpropd.c  |-  ( ph  ->  C  e.  Cat )
fucpropd.d  |-  ( ph  ->  D  e.  Cat )
Assertion
Ref Expression
fucpropd  |-  ( ph  ->  ( A FuncCat  C )  =  ( B FuncCat  D
) )

Proof of Theorem fucpropd
Dummy variables  a 
b  f  g  h  v  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fucpropd.1 . . . . 5  |-  ( ph  ->  (  Homf 
`  A )  =  (  Homf 
`  B ) )
2 fucpropd.2 . . . . 5  |-  ( ph  ->  (compf `  A )  =  (compf `  B ) )
3 fucpropd.3 . . . . 5  |-  ( ph  ->  (  Homf 
`  C )  =  (  Homf 
`  D ) )
4 fucpropd.4 . . . . 5  |-  ( ph  ->  (compf `  C )  =  (compf `  D ) )
5 fucpropd.a . . . . 5  |-  ( ph  ->  A  e.  Cat )
6 fucpropd.b . . . . 5  |-  ( ph  ->  B  e.  Cat )
7 fucpropd.c . . . . 5  |-  ( ph  ->  C  e.  Cat )
8 fucpropd.d . . . . 5  |-  ( ph  ->  D  e.  Cat )
91, 2, 3, 4, 5, 6, 7, 8funcpropd 14052 . . . 4  |-  ( ph  ->  ( A  Func  C
)  =  ( B 
Func  D ) )
109opeq2d 3951 . . 3  |-  ( ph  -> 
<. ( Base `  ndx ) ,  ( A  Func  C ) >.  =  <. (
Base `  ndx ) ,  ( B  Func  D
) >. )
111, 2, 3, 4, 5, 6, 7, 8natpropd 14128 . . . 4  |-  ( ph  ->  ( A Nat  C )  =  ( B Nat  D
) )
1211opeq2d 3951 . . 3  |-  ( ph  -> 
<. (  Hom  `  ndx ) ,  ( A Nat  C ) >.  =  <. (  Hom  `  ndx ) ,  ( B Nat  D )
>. )
139, 9xpeq12d 4862 . . . . 5  |-  ( ph  ->  ( ( A  Func  C )  X.  ( A 
Func  C ) )  =  ( ( B  Func  D )  X.  ( B 
Func  D ) ) )
149adantr 452 . . . . 5  |-  ( (
ph  /\  v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) ) )  ->  ( A  Func  C )  =  ( B 
Func  D ) )
15 nfv 1626 . . . . . 6  |-  F/ f ( ph  /\  (
v  e.  ( ( A  Func  C )  X.  ( A  Func  C
) )  /\  h  e.  ( A  Func  C
) ) )
16 nfcsb1v 3243 . . . . . . 7  |-  F/_ f [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )
1716a1i 11 . . . . . 6  |-  ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  ->  F/_ f [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )
18 fvex 5701 . . . . . . 7  |-  ( 1st `  v )  e.  _V
1918a1i 11 . . . . . 6  |-  ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  ->  ( 1st `  v
)  e.  _V )
20 nfv 1626 . . . . . . . 8  |-  F/ g ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )
21 nfcsb1v 3243 . . . . . . . . 9  |-  F/_ g [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )
2221a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  (
v  e.  ( ( A  Func  C )  X.  ( A  Func  C
) )  /\  h  e.  ( A  Func  C
) ) )  /\  f  =  ( 1st `  v ) )  ->  F/_ g [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )
23 fvex 5701 . . . . . . . . 9  |-  ( 2nd `  v )  e.  _V
2423a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  (
v  e.  ( ( A  Func  C )  X.  ( A  Func  C
) )  /\  h  e.  ( A  Func  C
) ) )  /\  f  =  ( 1st `  v ) )  -> 
( 2nd `  v
)  e.  _V )
2511ad3antrrr 711 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  ->  ( A Nat  C )  =  ( B Nat  D ) )
2625oveqd 6057 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  ->  (
g ( A Nat  C
) h )  =  ( g ( B Nat 
D ) h ) )
2725proplem3 13871 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  b  e.  ( g ( A Nat 
C ) h ) )  ->  ( f
( A Nat  C ) g )  =  ( f ( B Nat  D
) g ) )
281homfeqbas 13877 . . . . . . . . . . . 12  |-  ( ph  ->  ( Base `  A
)  =  ( Base `  B ) )
2928ad4antr 713 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( Base `  A )  =  ( Base `  B
) )
30 eqid 2404 . . . . . . . . . . . 12  |-  ( Base `  C )  =  (
Base `  C )
31 eqid 2404 . . . . . . . . . . . 12  |-  (  Hom  `  C )  =  (  Hom  `  C )
32 eqid 2404 . . . . . . . . . . . 12  |-  (comp `  C )  =  (comp `  C )
33 eqid 2404 . . . . . . . . . . . 12  |-  (comp `  D )  =  (comp `  D )
343ad5antr 715 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  (  Homf  `  C )  =  (  Homf 
`  D ) )
354ad5antr 715 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  (compf `  C
)  =  (compf `  D
) )
36 eqid 2404 . . . . . . . . . . . . . 14  |-  ( Base `  A )  =  (
Base `  A )
37 relfunc 14014 . . . . . . . . . . . . . . 15  |-  Rel  ( A  Func  C )
38 simpllr 736 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  f  =  ( 1st `  v
) )
39 simp-4r 744 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  (
v  e.  ( ( A  Func  C )  X.  ( A  Func  C
) )  /\  h  e.  ( A  Func  C
) ) )
4039simpld 446 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) ) )
41 xp1st 6335 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  ( ( A 
Func  C )  X.  ( A  Func  C ) )  ->  ( 1st `  v
)  e.  ( A 
Func  C ) )
4240, 41syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( 1st `  v )  e.  ( A  Func  C
) )
4338, 42eqeltrd 2478 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  f  e.  ( A  Func  C
) )
44 1st2ndbr 6355 . . . . . . . . . . . . . . 15  |-  ( ( Rel  ( A  Func  C )  /\  f  e.  ( A  Func  C
) )  ->  ( 1st `  f ) ( A  Func  C )
( 2nd `  f
) )
4537, 43, 44sylancr 645 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( 1st `  f ) ( A  Func  C )
( 2nd `  f
) )
4636, 30, 45funcf1 14018 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( 1st `  f ) : ( Base `  A
) --> ( Base `  C
) )
4746ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( 1st `  f
) `  x )  e.  ( Base `  C
) )
48 simplr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  g  =  ( 2nd `  v
) )
49 xp2nd 6336 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  ( ( A 
Func  C )  X.  ( A  Func  C ) )  ->  ( 2nd `  v
)  e.  ( A 
Func  C ) )
5040, 49syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( 2nd `  v )  e.  ( A  Func  C
) )
5148, 50eqeltrd 2478 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  g  e.  ( A  Func  C
) )
52 1st2ndbr 6355 . . . . . . . . . . . . . . 15  |-  ( ( Rel  ( A  Func  C )  /\  g  e.  ( A  Func  C
) )  ->  ( 1st `  g ) ( A  Func  C )
( 2nd `  g
) )
5337, 51, 52sylancr 645 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( 1st `  g ) ( A  Func  C )
( 2nd `  g
) )
5436, 30, 53funcf1 14018 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( 1st `  g ) : ( Base `  A
) --> ( Base `  C
) )
5554ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( 1st `  g
) `  x )  e.  ( Base `  C
) )
5639simprd 450 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  h  e.  ( A  Func  C
) )
57 1st2ndbr 6355 . . . . . . . . . . . . . . 15  |-  ( ( Rel  ( A  Func  C )  /\  h  e.  ( A  Func  C
) )  ->  ( 1st `  h ) ( A  Func  C )
( 2nd `  h
) )
5837, 56, 57sylancr 645 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( 1st `  h ) ( A  Func  C )
( 2nd `  h
) )
5936, 30, 58funcf1 14018 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  ( 1st `  h ) : ( Base `  A
) --> ( Base `  C
) )
6059ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( 1st `  h
) `  x )  e.  ( Base `  C
) )
61 eqid 2404 . . . . . . . . . . . . 13  |-  ( A Nat 
C )  =  ( A Nat  C )
62 simplrr 738 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  a  e.  ( f ( A Nat 
C ) g ) )
6361, 62nat1st2nd 14103 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  a  e.  ( <. ( 1st `  f
) ,  ( 2nd `  f ) >. ( A Nat  C ) <. ( 1st `  g ) ,  ( 2nd `  g
) >. ) )
64 simpr 448 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  x  e.  ( Base `  A
) )
6561, 63, 36, 31, 64natcl 14105 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
a `  x )  e.  ( ( ( 1st `  f ) `  x
) (  Hom  `  C
) ( ( 1st `  g ) `  x
) ) )
66 simplrl 737 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  b  e.  ( g ( A Nat 
C ) h ) )
6761, 66nat1st2nd 14103 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  b  e.  ( <. ( 1st `  g
) ,  ( 2nd `  g ) >. ( A Nat  C ) <. ( 1st `  h ) ,  ( 2nd `  h
) >. ) )
6861, 67, 36, 31, 64natcl 14105 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
b `  x )  e.  ( ( ( 1st `  g ) `  x
) (  Hom  `  C
) ( ( 1st `  h ) `  x
) ) )
6930, 31, 32, 33, 34, 35, 47, 55, 60, 65, 68comfeqval 13889 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  /\  x  e.  ( Base `  A
) )  ->  (
( b `  x
) ( <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) )  =  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) )
7029, 69mpteq12dva 4246 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  /\  (
b  e.  ( g ( A Nat  C ) h )  /\  a  e.  ( f ( A Nat 
C ) g ) ) )  ->  (
x  e.  ( Base `  A )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  C )
( ( 1st `  h
) `  x )
) ( a `  x ) ) )  =  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )
7126, 27, 70mpt2eq123dva 6094 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  ->  (
b  e.  ( g ( A Nat  C ) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  ( b  e.  ( g ( B Nat  D ) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )
72 csbeq1a 3219 . . . . . . . . . 10  |-  ( g  =  ( 2nd `  v
)  ->  ( b  e.  ( g ( B Nat 
D ) h ) ,  a  e.  ( f ( B Nat  D
) g )  |->  ( x  e.  ( Base `  B )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  D )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) )  =  [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g ( B Nat 
D ) h ) ,  a  e.  ( f ( B Nat  D
) g )  |->  ( x  e.  ( Base `  B )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  D )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) ) )
7372adantl 453 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  ->  (
b  e.  ( g ( B Nat  D ) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 2nd `  v )  /  g ]_ (
b  e.  ( g ( B Nat  D ) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )
7471, 73eqtrd 2436 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  /\  f  =  ( 1st `  v ) )  /\  g  =  ( 2nd `  v
) )  ->  (
b  e.  ( g ( A Nat  C ) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 2nd `  v )  /  g ]_ (
b  e.  ( g ( B Nat  D ) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )
7520, 22, 24, 74csbiedf 3248 . . . . . . 7  |-  ( ( ( ph  /\  (
v  e.  ( ( A  Func  C )  X.  ( A  Func  C
) )  /\  h  e.  ( A  Func  C
) ) )  /\  f  =  ( 1st `  v ) )  ->  [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 2nd `  v )  /  g ]_ (
b  e.  ( g ( B Nat  D ) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )
76 csbeq1a 3219 . . . . . . . 8  |-  ( f  =  ( 1st `  v
)  ->  [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 1st `  v )  /  f ]_ [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g ( B Nat 
D ) h ) ,  a  e.  ( f ( B Nat  D
) g )  |->  ( x  e.  ( Base `  B )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  D )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) ) )
7776adantl 453 . . . . . . 7  |-  ( ( ( ph  /\  (
v  e.  ( ( A  Func  C )  X.  ( A  Func  C
) )  /\  h  e.  ( A  Func  C
) ) )  /\  f  =  ( 1st `  v ) )  ->  [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 1st `  v )  /  f ]_ [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g ( B Nat 
D ) h ) ,  a  e.  ( f ( B Nat  D
) g )  |->  ( x  e.  ( Base `  B )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  D )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) ) )
7875, 77eqtrd 2436 . . . . . 6  |-  ( ( ( ph  /\  (
v  e.  ( ( A  Func  C )  X.  ( A  Func  C
) )  /\  h  e.  ( A  Func  C
) ) )  /\  f  =  ( 1st `  v ) )  ->  [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 1st `  v )  /  f ]_ [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g ( B Nat 
D ) h ) ,  a  e.  ( f ( B Nat  D
) g )  |->  ( x  e.  ( Base `  B )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  D )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) ) )
7915, 17, 19, 78csbiedf 3248 . . . . 5  |-  ( (
ph  /\  ( v  e.  ( ( A  Func  C )  X.  ( A 
Func  C ) )  /\  h  e.  ( A  Func  C ) ) )  ->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  [_ ( 1st `  v )  /  f ]_ [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g ( B Nat 
D ) h ) ,  a  e.  ( f ( B Nat  D
) g )  |->  ( x  e.  ( Base `  B )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  D )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) ) )
8013, 14, 79mpt2eq123dva 6094 . . . 4  |-  ( ph  ->  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) ) ,  h  e.  ( A 
Func  C )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )  =  ( v  e.  ( ( B  Func  D
)  X.  ( B 
Func  D ) ) ,  h  e.  ( B 
Func  D )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) )
8180opeq2d 3951 . . 3  |-  ( ph  -> 
<. (comp `  ndx ) ,  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) ) ,  h  e.  ( A 
Func  C )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >.  =  <. (comp `  ndx ) ,  ( v  e.  ( ( B  Func  D )  X.  ( B 
Func  D ) ) ,  h  e.  ( B 
Func  D )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >.
)
8210, 12, 81tpeq123d 3858 . 2  |-  ( ph  ->  { <. ( Base `  ndx ) ,  ( A  Func  C ) >. ,  <. (  Hom  `  ndx ) ,  ( A Nat  C )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( A 
Func  C )  X.  ( A  Func  C ) ) ,  h  e.  ( A  Func  C )  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. }  =  { <. ( Base `  ndx ) ,  ( B  Func  D
) >. ,  <. (  Hom  `  ndx ) ,  ( B Nat  D )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( B 
Func  D )  X.  ( B  Func  D ) ) ,  h  e.  ( B  Func  D )  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
83 eqid 2404 . . 3  |-  ( A FuncCat  C )  =  ( A FuncCat  C )
84 eqid 2404 . . 3  |-  ( A 
Func  C )  =  ( A  Func  C )
85 eqidd 2405 . . 3  |-  ( ph  ->  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) ) ,  h  e.  ( A 
Func  C )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )  =  ( v  e.  ( ( A  Func  C
)  X.  ( A 
Func  C ) ) ,  h  e.  ( A 
Func  C )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) )
8683, 84, 61, 36, 32, 5, 7, 85fucval 14110 . 2  |-  ( ph  ->  ( A FuncCat  C )  =  { <. ( Base `  ndx ) ,  ( A  Func  C ) >. ,  <. (  Hom  `  ndx ) ,  ( A Nat  C )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( A 
Func  C )  X.  ( A  Func  C ) ) ,  h  e.  ( A  Func  C )  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( A Nat  C
) h ) ,  a  e.  ( f ( A Nat  C ) g )  |->  ( x  e.  ( Base `  A
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  C
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
87 eqid 2404 . . 3  |-  ( B FuncCat  D )  =  ( B FuncCat  D )
88 eqid 2404 . . 3  |-  ( B 
Func  D )  =  ( B  Func  D )
89 eqid 2404 . . 3  |-  ( B Nat 
D )  =  ( B Nat  D )
90 eqid 2404 . . 3  |-  ( Base `  B )  =  (
Base `  B )
91 eqidd 2405 . . 3  |-  ( ph  ->  ( v  e.  ( ( B  Func  D
)  X.  ( B 
Func  D ) ) ,  h  e.  ( B 
Func  D )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )  =  ( v  e.  ( ( B  Func  D
)  X.  ( B 
Func  D ) ) ,  h  e.  ( B 
Func  D )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) )
9287, 88, 89, 90, 33, 6, 8, 91fucval 14110 . 2  |-  ( ph  ->  ( B FuncCat  D )  =  { <. ( Base `  ndx ) ,  ( B  Func  D ) >. ,  <. (  Hom  `  ndx ) ,  ( B Nat  D )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( B 
Func  D )  X.  ( B  Func  D ) ) ,  h  e.  ( B  Func  D )  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( B Nat  D
) h ) ,  a  e.  ( f ( B Nat  D ) g )  |->  ( x  e.  ( Base `  B
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  D
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
9382, 86, 923eqtr4d 2446 1  |-  ( ph  ->  ( A FuncCat  C )  =  ( B FuncCat  D
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   F/_wnfc 2527   _Vcvv 2916   [_csb 3211   {ctp 3776   <.cop 3777   class class class wbr 4172    e. cmpt 4226    X. cxp 4835   Rel wrel 4842   ` cfv 5413  (class class class)co 6040    e. cmpt2 6042   1stc1st 6306   2ndc2nd 6307   ndxcnx 13421   Basecbs 13424    Hom chom 13495  compcco 13496   Catccat 13844    Homf chomf 13846  compfccomf 13847    Func cfunc 14006   Nat cnat 14093   FuncCat cfuc 14094
This theorem is referenced by:  oyoncl  14322
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-map 6979  df-ixp 7023  df-cat 13848  df-cid 13849  df-homf 13850  df-comf 13851  df-func 14010  df-nat 14095  df-fuc 14096
  Copyright terms: Public domain W3C validator