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

Theorem invfuc 13897
Description: If  V
( x ) is an inverse to  U ( x ) for each  x, and  U is a natural transformation, then  V is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017.)
Hypotheses
Ref Expression
fuciso.q  |-  Q  =  ( C FuncCat  D )
fuciso.b  |-  B  =  ( Base `  C
)
fuciso.n  |-  N  =  ( C Nat  D )
fuciso.f  |-  ( ph  ->  F  e.  ( C 
Func  D ) )
fuciso.g  |-  ( ph  ->  G  e.  ( C 
Func  D ) )
fucinv.i  |-  I  =  (Inv `  Q )
fucinv.j  |-  J  =  (Inv `  D )
invfuc.u  |-  ( ph  ->  U  e.  ( F N G ) )
invfuc.v  |-  ( (
ph  /\  x  e.  B )  ->  ( U `  x )
( ( ( 1st `  F ) `  x
) J ( ( 1st `  G ) `
 x ) ) X )
Assertion
Ref Expression
invfuc  |-  ( ph  ->  U ( F I G ) ( x  e.  B  |->  X ) )
Distinct variable groups:    x, B    x, C    x, D    x, I    x, F    x, G    x, J    x, N    ph, x    x, Q    x, U
Allowed substitution hint:    X( x)

Proof of Theorem invfuc
Dummy variables  y 
f  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 invfuc.u . 2  |-  ( ph  ->  U  e.  ( F N G ) )
2 invfuc.v . . . . . . . 8  |-  ( (
ph  /\  x  e.  B )  ->  ( U `  x )
( ( ( 1st `  F ) `  x
) J ( ( 1st `  G ) `
 x ) ) X )
3 eqid 2316 . . . . . . . . . 10  |-  ( Base `  D )  =  (
Base `  D )
4 fucinv.j . . . . . . . . . 10  |-  J  =  (Inv `  D )
5 fuciso.f . . . . . . . . . . . . 13  |-  ( ph  ->  F  e.  ( C 
Func  D ) )
6 funcrcl 13786 . . . . . . . . . . . . 13  |-  ( F  e.  ( C  Func  D )  ->  ( C  e.  Cat  /\  D  e. 
Cat ) )
75, 6syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( C  e.  Cat  /\  D  e.  Cat )
)
87simprd 449 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  Cat )
98adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  B )  ->  D  e.  Cat )
10 fuciso.b . . . . . . . . . . . 12  |-  B  =  ( Base `  C
)
11 relfunc 13785 . . . . . . . . . . . . 13  |-  Rel  ( C  Func  D )
12 1st2ndbr 6211 . . . . . . . . . . . . 13  |-  ( ( Rel  ( C  Func  D )  /\  F  e.  ( C  Func  D
) )  ->  ( 1st `  F ) ( C  Func  D )
( 2nd `  F
) )
1311, 5, 12sylancr 644 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  F
) ( C  Func  D ) ( 2nd `  F
) )
1410, 3, 13funcf1 13789 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  F
) : B --> ( Base `  D ) )
1514ffvelrnda 5703 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  B )  ->  (
( 1st `  F
) `  x )  e.  ( Base `  D
) )
16 fuciso.g . . . . . . . . . . . . 13  |-  ( ph  ->  G  e.  ( C 
Func  D ) )
17 1st2ndbr 6211 . . . . . . . . . . . . 13  |-  ( ( Rel  ( C  Func  D )  /\  G  e.  ( C  Func  D
) )  ->  ( 1st `  G ) ( C  Func  D )
( 2nd `  G
) )
1811, 16, 17sylancr 644 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  G
) ( C  Func  D ) ( 2nd `  G
) )
1910, 3, 18funcf1 13789 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  G
) : B --> ( Base `  D ) )
2019ffvelrnda 5703 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  B )  ->  (
( 1st `  G
) `  x )  e.  ( Base `  D
) )
21 eqid 2316 . . . . . . . . . 10  |-  (  Hom  `  D )  =  (  Hom  `  D )
223, 4, 9, 15, 20, 21invss 13712 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  B )  ->  (
( ( 1st `  F
) `  x ) J ( ( 1st `  G ) `  x
) )  C_  (
( ( ( 1st `  F ) `  x
) (  Hom  `  D
) ( ( 1st `  G ) `  x
) )  X.  (
( ( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) ) )
2322ssbrd 4101 . . . . . . . 8  |-  ( (
ph  /\  x  e.  B )  ->  (
( U `  x
) ( ( ( 1st `  F ) `
 x ) J ( ( 1st `  G
) `  x )
) X  ->  ( U `  x )
( ( ( ( 1st `  F ) `
 x ) (  Hom  `  D )
( ( 1st `  G
) `  x )
)  X.  ( ( ( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) ) X ) )
242, 23mpd 14 . . . . . . 7  |-  ( (
ph  /\  x  e.  B )  ->  ( U `  x )
( ( ( ( 1st `  F ) `
 x ) (  Hom  `  D )
( ( 1st `  G
) `  x )
)  X.  ( ( ( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) ) X )
25 brxp 4757 . . . . . . . 8  |-  ( ( U `  x ) ( ( ( ( 1st `  F ) `
 x ) (  Hom  `  D )
( ( 1st `  G
) `  x )
)  X.  ( ( ( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) ) X  <->  ( ( U `  x )  e.  ( ( ( 1st `  F ) `  x
) (  Hom  `  D
) ( ( 1st `  G ) `  x
) )  /\  X  e.  ( ( ( 1st `  G ) `  x
) (  Hom  `  D
) ( ( 1st `  F ) `  x
) ) ) )
2625simprbi 450 . . . . . . 7  |-  ( ( U `  x ) ( ( ( ( 1st `  F ) `
 x ) (  Hom  `  D )
( ( 1st `  G
) `  x )
)  X.  ( ( ( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) ) X  ->  X  e.  ( (
( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) )
2724, 26syl 15 . . . . . 6  |-  ( (
ph  /\  x  e.  B )  ->  X  e.  ( ( ( 1st `  G ) `  x
) (  Hom  `  D
) ( ( 1st `  F ) `  x
) ) )
2827ralrimiva 2660 . . . . 5  |-  ( ph  ->  A. x  e.  B  X  e.  ( (
( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) )
29 fvex 5577 . . . . . . 7  |-  ( Base `  C )  e.  _V
3010, 29eqeltri 2386 . . . . . 6  |-  B  e. 
_V
31 mptelixpg 6896 . . . . . 6  |-  ( B  e.  _V  ->  (
( x  e.  B  |->  X )  e.  X_ x  e.  B  (
( ( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
)  <->  A. x  e.  B  X  e.  ( (
( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) ) )
3230, 31ax-mp 8 . . . . 5  |-  ( ( x  e.  B  |->  X )  e.  X_ x  e.  B  ( (
( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
)  <->  A. x  e.  B  X  e.  ( (
( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) )
3328, 32sylibr 203 . . . 4  |-  ( ph  ->  ( x  e.  B  |->  X )  e.  X_ x  e.  B  (
( ( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) )
34 nfcv 2452 . . . . 5  |-  F/_ y
( ( ( 1st `  G ) `  x
) (  Hom  `  D
) ( ( 1st `  F ) `  x
) )
35 nfcv 2452 . . . . 5  |-  F/_ x
( ( ( 1st `  G ) `  y
) (  Hom  `  D
) ( ( 1st `  F ) `  y
) )
36 fveq2 5563 . . . . . 6  |-  ( x  =  y  ->  (
( 1st `  G
) `  x )  =  ( ( 1st `  G ) `  y
) )
37 fveq2 5563 . . . . . 6  |-  ( x  =  y  ->  (
( 1st `  F
) `  x )  =  ( ( 1st `  F ) `  y
) )
3836, 37oveq12d 5918 . . . . 5  |-  ( x  =  y  ->  (
( ( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
)  =  ( ( ( 1st `  G
) `  y )
(  Hom  `  D ) ( ( 1st `  F
) `  y )
) )
3934, 35, 38cbvixp 6876 . . . 4  |-  X_ x  e.  B  ( (
( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
)  =  X_ y  e.  B  ( (
( 1st `  G
) `  y )
(  Hom  `  D ) ( ( 1st `  F
) `  y )
)
4033, 39syl6eleq 2406 . . 3  |-  ( ph  ->  ( x  e.  B  |->  X )  e.  X_ y  e.  B  (
( ( 1st `  G
) `  y )
(  Hom  `  D ) ( ( 1st `  F
) `  y )
) )
41 simpr2 962 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  z  e.  B )
42 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  B )  ->  x  e.  B )
43 eqid 2316 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  B  |->  X )  =  ( x  e.  B  |->  X )
4443fvmpt2 5646 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  B  /\  X  e.  ( (
( 1st `  G
) `  x )
(  Hom  `  D ) ( ( 1st `  F
) `  x )
) )  ->  (
( x  e.  B  |->  X ) `  x
)  =  X )
4542, 27, 44syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  B )  ->  (
( x  e.  B  |->  X ) `  x
)  =  X )
462, 45breqtrrd 4086 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  B )  ->  ( U `  x )
( ( ( 1st `  F ) `  x
) J ( ( 1st `  G ) `
 x ) ) ( ( x  e.  B  |->  X ) `  x ) )
4746ralrimiva 2660 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. x  e.  B  ( U `  x ) ( ( ( 1st `  F ) `  x
) J ( ( 1st `  G ) `
 x ) ) ( ( x  e.  B  |->  X ) `  x ) )
4847adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  A. x  e.  B  ( U `  x ) ( ( ( 1st `  F
) `  x ) J ( ( 1st `  G ) `  x
) ) ( ( x  e.  B  |->  X ) `  x ) )
49 nfcv 2452 . . . . . . . . . . . . . . . 16  |-  F/_ x
( U `  z
)
50 nfcv 2452 . . . . . . . . . . . . . . . 16  |-  F/_ x
( ( ( 1st `  F ) `  z
) J ( ( 1st `  G ) `
 z ) )
51 nffvmpt1 5571 . . . . . . . . . . . . . . . 16  |-  F/_ x
( ( x  e.  B  |->  X ) `  z )
5249, 50, 51nfbr 4104 . . . . . . . . . . . . . . 15  |-  F/ x
( U `  z
) ( ( ( 1st `  F ) `
 z ) J ( ( 1st `  G
) `  z )
) ( ( x  e.  B  |->  X ) `
 z )
53 fveq2 5563 . . . . . . . . . . . . . . . 16  |-  ( x  =  z  ->  ( U `  x )  =  ( U `  z ) )
54 fveq2 5563 . . . . . . . . . . . . . . . . 17  |-  ( x  =  z  ->  (
( 1st `  F
) `  x )  =  ( ( 1st `  F ) `  z
) )
55 fveq2 5563 . . . . . . . . . . . . . . . . 17  |-  ( x  =  z  ->  (
( 1st `  G
) `  x )  =  ( ( 1st `  G ) `  z
) )
5654, 55oveq12d 5918 . . . . . . . . . . . . . . . 16  |-  ( x  =  z  ->  (
( ( 1st `  F
) `  x ) J ( ( 1st `  G ) `  x
) )  =  ( ( ( 1st `  F
) `  z ) J ( ( 1st `  G ) `  z
) ) )
57 fveq2 5563 . . . . . . . . . . . . . . . 16  |-  ( x  =  z  ->  (
( x  e.  B  |->  X ) `  x
)  =  ( ( x  e.  B  |->  X ) `  z ) )
5853, 56, 57breq123d 4074 . . . . . . . . . . . . . . 15  |-  ( x  =  z  ->  (
( U `  x
) ( ( ( 1st `  F ) `
 x ) J ( ( 1st `  G
) `  x )
) ( ( x  e.  B  |->  X ) `
 x )  <->  ( U `  z ) ( ( ( 1st `  F
) `  z ) J ( ( 1st `  G ) `  z
) ) ( ( x  e.  B  |->  X ) `  z ) ) )
5952, 58rspc 2912 . . . . . . . . . . . . . 14  |-  ( z  e.  B  ->  ( A. x  e.  B  ( U `  x ) ( ( ( 1st `  F ) `  x
) J ( ( 1st `  G ) `
 x ) ) ( ( x  e.  B  |->  X ) `  x )  ->  ( U `  z )
( ( ( 1st `  F ) `  z
) J ( ( 1st `  G ) `
 z ) ) ( ( x  e.  B  |->  X ) `  z ) ) )
6041, 48, 59sylc 56 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( U `  z )
( ( ( 1st `  F ) `  z
) J ( ( 1st `  G ) `
 z ) ) ( ( x  e.  B  |->  X ) `  z ) )
618adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  D  e.  Cat )
6214adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( 1st `  F ) : B --> ( Base `  D
) )
6362, 41ffvelrnd 5704 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( 1st `  F
) `  z )  e.  ( Base `  D
) )
6419adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( 1st `  G ) : B --> ( Base `  D
) )
6564, 41ffvelrnd 5704 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( 1st `  G
) `  z )  e.  ( Base `  D
) )
66 eqid 2316 . . . . . . . . . . . . . 14  |-  (Sect `  D )  =  (Sect `  D )
673, 4, 61, 63, 65, 66isinv 13711 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( U `  z
) ( ( ( 1st `  F ) `
 z ) J ( ( 1st `  G
) `  z )
) ( ( x  e.  B  |->  X ) `
 z )  <->  ( ( U `  z )
( ( ( 1st `  F ) `  z
) (Sect `  D
) ( ( 1st `  G ) `  z
) ) ( ( x  e.  B  |->  X ) `  z )  /\  ( ( x  e.  B  |->  X ) `
 z ) ( ( ( 1st `  G
) `  z )
(Sect `  D )
( ( 1st `  F
) `  z )
) ( U `  z ) ) ) )
6860, 67mpbid 201 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( U `  z
) ( ( ( 1st `  F ) `
 z ) (Sect `  D ) ( ( 1st `  G ) `
 z ) ) ( ( x  e.  B  |->  X ) `  z )  /\  (
( x  e.  B  |->  X ) `  z
) ( ( ( 1st `  G ) `
 z ) (Sect `  D ) ( ( 1st `  F ) `
 z ) ) ( U `  z
) ) )
6968simpld 445 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( U `  z )
( ( ( 1st `  F ) `  z
) (Sect `  D
) ( ( 1st `  G ) `  z
) ) ( ( x  e.  B  |->  X ) `  z ) )
70 eqid 2316 . . . . . . . . . . . 12  |-  (comp `  D )  =  (comp `  D )
71 eqid 2316 . . . . . . . . . . . 12  |-  ( Id
`  D )  =  ( Id `  D
)
723, 21, 70, 71, 66, 61, 63, 65issect 13705 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( U `  z
) ( ( ( 1st `  F ) `
 z ) (Sect `  D ) ( ( 1st `  G ) `
 z ) ) ( ( x  e.  B  |->  X ) `  z )  <->  ( ( U `  z )  e.  ( ( ( 1st `  F ) `  z
) (  Hom  `  D
) ( ( 1st `  G ) `  z
) )  /\  (
( x  e.  B  |->  X ) `  z
)  e.  ( ( ( 1st `  G
) `  z )
(  Hom  `  D ) ( ( 1st `  F
) `  z )
)  /\  ( (
( x  e.  B  |->  X ) `  z
) ( <. (
( 1st `  F
) `  z ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( U `
 z ) )  =  ( ( Id
`  D ) `  ( ( 1st `  F
) `  z )
) ) ) )
7369, 72mpbid 201 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( U `  z
)  e.  ( ( ( 1st `  F
) `  z )
(  Hom  `  D ) ( ( 1st `  G
) `  z )
)  /\  ( (
x  e.  B  |->  X ) `  z )  e.  ( ( ( 1st `  G ) `
 z ) (  Hom  `  D )
( ( 1st `  F
) `  z )
)  /\  ( (
( x  e.  B  |->  X ) `  z
) ( <. (
( 1st `  F
) `  z ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( U `
 z ) )  =  ( ( Id
`  D ) `  ( ( 1st `  F
) `  z )
) ) )
7473simp3d 969 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( x  e.  B  |->  X ) `  z ) ( <.
( ( 1st `  F
) `  z ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( U `
 z ) )  =  ( ( Id
`  D ) `  ( ( 1st `  F
) `  z )
) )
7574oveq1d 5915 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( ( x  e.  B  |->  X ) `
 z ) (
<. ( ( 1st `  F
) `  z ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( U `
 z ) ) ( <. ( ( 1st `  F ) `  y
) ,  ( ( 1st `  F ) `
 z ) >.
(comp `  D )
( ( 1st `  F
) `  z )
) ( ( y ( 2nd `  F
) z ) `  f ) )  =  ( ( ( Id
`  D ) `  ( ( 1st `  F
) `  z )
) ( <. (
( 1st `  F
) `  y ) ,  ( ( 1st `  F ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( y ( 2nd `  F
) z ) `  f ) ) )
76 simpr1 961 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  y  e.  B )
7762, 76ffvelrnd 5704 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( 1st `  F
) `  y )  e.  ( Base `  D
) )
78 eqid 2316 . . . . . . . . . . 11  |-  (  Hom  `  C )  =  (  Hom  `  C )
7913adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( 1st `  F ) ( C  Func  D )
( 2nd `  F
) )
8010, 78, 21, 79, 76, 41funcf2 13791 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
y ( 2nd `  F
) z ) : ( y (  Hom  `  C ) z ) --> ( ( ( 1st `  F ) `  y
) (  Hom  `  D
) ( ( 1st `  F ) `  z
) ) )
81 simpr3 963 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  f  e.  ( y (  Hom  `  C ) z ) )
8280, 81ffvelrnd 5704 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( y ( 2nd `  F ) z ) `
 f )  e.  ( ( ( 1st `  F ) `  y
) (  Hom  `  D
) ( ( 1st `  F ) `  z
) ) )
833, 21, 71, 61, 77, 70, 63, 82catlid 13634 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( Id `  D ) `  (
( 1st `  F
) `  z )
) ( <. (
( 1st `  F
) `  y ) ,  ( ( 1st `  F ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( y ( 2nd `  F
) z ) `  f ) )  =  ( ( y ( 2nd `  F ) z ) `  f
) )
8475, 83eqtr2d 2349 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( y ( 2nd `  F ) z ) `
 f )  =  ( ( ( ( x  e.  B  |->  X ) `  z ) ( <. ( ( 1st `  F ) `  z
) ,  ( ( 1st `  G ) `
 z ) >.
(comp `  D )
( ( 1st `  F
) `  z )
) ( U `  z ) ) (
<. ( ( 1st `  F
) `  y ) ,  ( ( 1st `  F ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( y ( 2nd `  F
) z ) `  f ) ) )
85 fuciso.n . . . . . . . . 9  |-  N  =  ( C Nat  D )
861adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  U  e.  ( F N G ) )
8785, 86nat1st2nd 13874 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  U  e.  ( <. ( 1st `  F
) ,  ( 2nd `  F ) >. N <. ( 1st `  G ) ,  ( 2nd `  G
) >. ) )
8885, 87, 10, 21, 41natcl 13876 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( U `  z )  e.  ( ( ( 1st `  F ) `  z
) (  Hom  `  D
) ( ( 1st `  G ) `  z
) ) )
8973simp2d 968 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( x  e.  B  |->  X ) `  z
)  e.  ( ( ( 1st `  G
) `  z )
(  Hom  `  D ) ( ( 1st `  F
) `  z )
) )
903, 21, 70, 61, 77, 63, 65, 82, 88, 63, 89catass 13637 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( ( x  e.  B  |->  X ) `
 z ) (
<. ( ( 1st `  F
) `  z ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( U `
 z ) ) ( <. ( ( 1st `  F ) `  y
) ,  ( ( 1st `  F ) `
 z ) >.
(comp `  D )
( ( 1st `  F
) `  z )
) ( ( y ( 2nd `  F
) z ) `  f ) )  =  ( ( ( x  e.  B  |->  X ) `
 z ) (
<. ( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( U `  z ) ( <. ( ( 1st `  F ) `  y
) ,  ( ( 1st `  F ) `
 z ) >.
(comp `  D )
( ( 1st `  G
) `  z )
) ( ( y ( 2nd `  F
) z ) `  f ) ) ) )
9185, 87, 10, 78, 70, 76, 41, 81nati 13878 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( U `  z
) ( <. (
( 1st `  F
) `  y ) ,  ( ( 1st `  F ) `  z
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( ( y ( 2nd `  F
) z ) `  f ) )  =  ( ( ( y ( 2nd `  G
) z ) `  f ) ( <.
( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) )
9291oveq2d 5916 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( x  e.  B  |->  X ) `  z ) ( <.
( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( U `  z ) ( <. ( ( 1st `  F ) `  y
) ,  ( ( 1st `  F ) `
 z ) >.
(comp `  D )
( ( 1st `  G
) `  z )
) ( ( y ( 2nd `  F
) z ) `  f ) ) )  =  ( ( ( x  e.  B  |->  X ) `  z ) ( <. ( ( 1st `  F ) `  y
) ,  ( ( 1st `  G ) `
 z ) >.
(comp `  D )
( ( 1st `  F
) `  z )
) ( ( ( y ( 2nd `  G
) z ) `  f ) ( <.
( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) ) )
9384, 90, 923eqtrd 2352 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( y ( 2nd `  F ) z ) `
 f )  =  ( ( ( x  e.  B  |->  X ) `
 z ) (
<. ( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( ( y ( 2nd `  G ) z ) `
 f ) (
<. ( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) ) )
9493oveq1d 5915 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( y ( 2nd `  F ) z ) `  f
) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  F ) `  y
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( x  e.  B  |->  X ) `  y ) )  =  ( ( ( ( x  e.  B  |->  X ) `  z ) ( <.
( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( ( y ( 2nd `  G ) z ) `
 f ) (
<. ( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) ) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  F ) `  y
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( x  e.  B  |->  X ) `  y ) ) )
9564, 76ffvelrnd 5704 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( 1st `  G
) `  y )  e.  ( Base `  D
) )
96 nfcv 2452 . . . . . . . . . . . . 13  |-  F/_ x
( U `  y
)
97 nfcv 2452 . . . . . . . . . . . . 13  |-  F/_ x
( ( ( 1st `  F ) `  y
) J ( ( 1st `  G ) `
 y ) )
98 nffvmpt1 5571 . . . . . . . . . . . . 13  |-  F/_ x
( ( x  e.  B  |->  X ) `  y )
9996, 97, 98nfbr 4104 . . . . . . . . . . . 12  |-  F/ x
( U `  y
) ( ( ( 1st `  F ) `
 y ) J ( ( 1st `  G
) `  y )
) ( ( x  e.  B  |->  X ) `
 y )
100 fveq2 5563 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( U `  x )  =  ( U `  y ) )
10137, 36oveq12d 5918 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( ( 1st `  F
) `  x ) J ( ( 1st `  G ) `  x
) )  =  ( ( ( 1st `  F
) `  y ) J ( ( 1st `  G ) `  y
) ) )
102 fveq2 5563 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( x  e.  B  |->  X ) `  x
)  =  ( ( x  e.  B  |->  X ) `  y ) )
103100, 101, 102breq123d 4074 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( U `  x
) ( ( ( 1st `  F ) `
 x ) J ( ( 1st `  G
) `  x )
) ( ( x  e.  B  |->  X ) `
 x )  <->  ( U `  y ) ( ( ( 1st `  F
) `  y ) J ( ( 1st `  G ) `  y
) ) ( ( x  e.  B  |->  X ) `  y ) ) )
10499, 103rspc 2912 . . . . . . . . . . 11  |-  ( y  e.  B  ->  ( A. x  e.  B  ( U `  x ) ( ( ( 1st `  F ) `  x
) J ( ( 1st `  G ) `
 x ) ) ( ( x  e.  B  |->  X ) `  x )  ->  ( U `  y )
( ( ( 1st `  F ) `  y
) J ( ( 1st `  G ) `
 y ) ) ( ( x  e.  B  |->  X ) `  y ) ) )
10576, 48, 104sylc 56 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( U `  y )
( ( ( 1st `  F ) `  y
) J ( ( 1st `  G ) `
 y ) ) ( ( x  e.  B  |->  X ) `  y ) )
1063, 4, 61, 77, 95, 66isinv 13711 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( U `  y
) ( ( ( 1st `  F ) `
 y ) J ( ( 1st `  G
) `  y )
) ( ( x  e.  B  |->  X ) `
 y )  <->  ( ( U `  y )
( ( ( 1st `  F ) `  y
) (Sect `  D
) ( ( 1st `  G ) `  y
) ) ( ( x  e.  B  |->  X ) `  y )  /\  ( ( x  e.  B  |->  X ) `
 y ) ( ( ( 1st `  G
) `  y )
(Sect `  D )
( ( 1st `  F
) `  y )
) ( U `  y ) ) ) )
107105, 106mpbid 201 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( U `  y
) ( ( ( 1st `  F ) `
 y ) (Sect `  D ) ( ( 1st `  G ) `
 y ) ) ( ( x  e.  B  |->  X ) `  y )  /\  (
( x  e.  B  |->  X ) `  y
) ( ( ( 1st `  G ) `
 y ) (Sect `  D ) ( ( 1st `  F ) `
 y ) ) ( U `  y
) ) )
108107simprd 449 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( x  e.  B  |->  X ) `  y
) ( ( ( 1st `  G ) `
 y ) (Sect `  D ) ( ( 1st `  F ) `
 y ) ) ( U `  y
) )
1093, 21, 70, 71, 66, 61, 95, 77issect 13705 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( x  e.  B  |->  X ) `  y ) ( ( ( 1st `  G
) `  y )
(Sect `  D )
( ( 1st `  F
) `  y )
) ( U `  y )  <->  ( (
( x  e.  B  |->  X ) `  y
)  e.  ( ( ( 1st `  G
) `  y )
(  Hom  `  D ) ( ( 1st `  F
) `  y )
)  /\  ( U `  y )  e.  ( ( ( 1st `  F
) `  y )
(  Hom  `  D ) ( ( 1st `  G
) `  y )
)  /\  ( ( U `  y )
( <. ( ( 1st `  G ) `  y
) ,  ( ( 1st `  F ) `
 y ) >.
(comp `  D )
( ( 1st `  G
) `  y )
) ( ( x  e.  B  |->  X ) `
 y ) )  =  ( ( Id
`  D ) `  ( ( 1st `  G
) `  y )
) ) ) )
110108, 109mpbid 201 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( x  e.  B  |->  X ) `  y )  e.  ( ( ( 1st `  G
) `  y )
(  Hom  `  D ) ( ( 1st `  F
) `  y )
)  /\  ( U `  y )  e.  ( ( ( 1st `  F
) `  y )
(  Hom  `  D ) ( ( 1st `  G
) `  y )
)  /\  ( ( U `  y )
( <. ( ( 1st `  G ) `  y
) ,  ( ( 1st `  F ) `
 y ) >.
(comp `  D )
( ( 1st `  G
) `  y )
) ( ( x  e.  B  |->  X ) `
 y ) )  =  ( ( Id
`  D ) `  ( ( 1st `  G
) `  y )
) ) )
111110simp1d 967 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( x  e.  B  |->  X ) `  y
)  e.  ( ( ( 1st `  G
) `  y )
(  Hom  `  D ) ( ( 1st `  F
) `  y )
) )
112110simp2d 968 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( U `  y )  e.  ( ( ( 1st `  F ) `  y
) (  Hom  `  D
) ( ( 1st `  G ) `  y
) ) )
11318adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( 1st `  G ) ( C  Func  D )
( 2nd `  G
) )
11410, 78, 21, 113, 76, 41funcf2 13791 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
y ( 2nd `  G
) z ) : ( y (  Hom  `  C ) z ) --> ( ( ( 1st `  G ) `  y
) (  Hom  `  D
) ( ( 1st `  G ) `  z
) ) )
115114, 81ffvelrnd 5704 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( y ( 2nd `  G ) z ) `
 f )  e.  ( ( ( 1st `  G ) `  y
) (  Hom  `  D
) ( ( 1st `  G ) `  z
) ) )
1163, 21, 70, 61, 77, 95, 65, 112, 115catcocl 13636 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( y ( 2nd `  G ) z ) `  f
) ( <. (
( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) )  e.  ( ( ( 1st `  F ) `
 y ) (  Hom  `  D )
( ( 1st `  G
) `  z )
) )
1173, 21, 70, 61, 95, 77, 65, 111, 116, 63, 89catass 13637 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( ( x  e.  B  |->  X ) `
 z ) (
<. ( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( ( y ( 2nd `  G ) z ) `
 f ) (
<. ( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) ) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  F ) `  y
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( x  e.  B  |->  X ) `  y ) )  =  ( ( ( x  e.  B  |->  X ) `  z
) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( ( ( y ( 2nd `  G ) z ) `  f
) ( <. (
( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) ( <. ( ( 1st `  G ) `  y
) ,  ( ( 1st `  F ) `
 y ) >.
(comp `  D )
( ( 1st `  G
) `  z )
) ( ( x  e.  B  |->  X ) `
 y ) ) ) )
11885, 87, 10, 21, 76natcl 13876 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  ( U `  y )  e.  ( ( ( 1st `  F ) `  y
) (  Hom  `  D
) ( ( 1st `  G ) `  y
) ) )
1193, 21, 70, 61, 95, 77, 95, 111, 118, 65, 115catass 13637 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( ( y ( 2nd `  G
) z ) `  f ) ( <.
( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) ( <. ( ( 1st `  G ) `  y
) ,  ( ( 1st `  F ) `
 y ) >.
(comp `  D )
( ( 1st `  G
) `  z )
) ( ( x  e.  B  |->  X ) `
 y ) )  =  ( ( ( y ( 2nd `  G
) z ) `  f ) ( <.
( ( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( ( U `  y ) ( <. ( ( 1st `  G ) `  y
) ,  ( ( 1st `  F ) `
 y ) >.
(comp `  D )
( ( 1st `  G
) `  y )
) ( ( x  e.  B  |->  X ) `
 y ) ) ) )
120110simp3d 969 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( U `  y
) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  F ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  y
) ) ( ( x  e.  B  |->  X ) `  y ) )  =  ( ( Id `  D ) `
 ( ( 1st `  G ) `  y
) ) )
121120oveq2d 5916 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( y ( 2nd `  G ) z ) `  f
) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( ( U `  y ) ( <. ( ( 1st `  G ) `  y
) ,  ( ( 1st `  F ) `
 y ) >.
(comp `  D )
( ( 1st `  G
) `  y )
) ( ( x  e.  B  |->  X ) `
 y ) ) )  =  ( ( ( y ( 2nd `  G ) z ) `
 f ) (
<. ( ( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( ( Id `  D ) `
 ( ( 1st `  G ) `  y
) ) ) )
1223, 21, 71, 61, 95, 70, 65, 115catrid 13635 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( y ( 2nd `  G ) z ) `  f
) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( ( Id `  D ) `
 ( ( 1st `  G ) `  y
) ) )  =  ( ( y ( 2nd `  G ) z ) `  f
) )
123119, 121, 1223eqtrd 2352 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( ( y ( 2nd `  G
) z ) `  f ) ( <.
( ( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) ( <. ( ( 1st `  G ) `  y
) ,  ( ( 1st `  F ) `
 y ) >.
(comp `  D )
( ( 1st `  G
) `  z )
) ( ( x  e.  B  |->  X ) `
 y ) )  =  ( ( y ( 2nd `  G
) z ) `  f ) )
124123oveq2d 5916 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( x  e.  B  |->  X ) `  z ) ( <.
( ( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( ( ( y ( 2nd `  G ) z ) `  f
) ( <. (
( 1st `  F
) `  y ) ,  ( ( 1st `  G ) `  y
) >. (comp `  D
) ( ( 1st `  G ) `  z
) ) ( U `
 y ) ) ( <. ( ( 1st `  G ) `  y
) ,  ( ( 1st `  F ) `
 y ) >.
(comp `  D )
( ( 1st `  G
) `  z )
) ( ( x  e.  B  |->  X ) `
 y ) ) )  =  ( ( ( x  e.  B  |->  X ) `  z
) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( y ( 2nd `  G
) z ) `  f ) ) )
12594, 117, 1243eqtrrd 2353 . . . 4  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B  /\  f  e.  ( y (  Hom  `  C ) z ) ) )  ->  (
( ( x  e.  B  |->  X ) `  z ) ( <.
( ( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( y ( 2nd `  G
) z ) `  f ) )  =  ( ( ( y ( 2nd `  F
) z ) `  f ) ( <.
( ( 1st `  G
) `  y ) ,  ( ( 1st `  F ) `  y
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( x  e.  B  |->  X ) `  y ) ) )
126125ralrimivvva 2670 . . 3  |-  ( ph  ->  A. y  e.  B  A. z  e.  B  A. f  e.  (
y (  Hom  `  C
) z ) ( ( ( x  e.  B  |->  X ) `  z ) ( <.
( ( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( y ( 2nd `  G
) z ) `  f ) )  =  ( ( ( y ( 2nd `  F
) z ) `  f ) ( <.
( ( 1st `  G
) `  y ) ,  ( ( 1st `  F ) `  y
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( x  e.  B  |->  X ) `  y ) ) )
12785, 10, 78, 21, 70, 16, 5isnat2 13871 . . 3  |-  ( ph  ->  ( ( x  e.  B  |->  X )  e.  ( G N F )  <->  ( ( x  e.  B  |->  X )  e.  X_ y  e.  B  ( ( ( 1st `  G ) `  y
) (  Hom  `  D
) ( ( 1st `  F ) `  y
) )  /\  A. y  e.  B  A. z  e.  B  A. f  e.  ( y
(  Hom  `  C ) z ) ( ( ( x  e.  B  |->  X ) `  z
) ( <. (
( 1st `  G
) `  y ) ,  ( ( 1st `  G ) `  z
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( y ( 2nd `  G
) z ) `  f ) )  =  ( ( ( y ( 2nd `  F
) z ) `  f ) ( <.
( ( 1st `  G
) `  y ) ,  ( ( 1st `  F ) `  y
) >. (comp `  D
) ( ( 1st `  F ) `  z
) ) ( ( x  e.  B  |->  X ) `  y ) ) ) ) )
12840, 126, 127mpbir2and 888 . 2  |-  ( ph  ->  ( x  e.  B  |->  X )  e.  ( G N F ) )
129 nfv 1610 . . . 4  |-  F/ y ( U `  x
) ( ( ( 1st `  F ) `
 x ) J ( ( 1st `  G
) `  x )
) ( ( x  e.  B  |->  X ) `
 x )
130129, 99, 103cbvral 2794 . . 3  |-  ( A. x  e.  B  ( U `  x )
( ( ( 1st `  F ) `  x
) J ( ( 1st `  G ) `
 x ) ) ( ( x  e.  B  |->  X ) `  x )  <->  A. y  e.  B  ( U `  y ) ( ( ( 1st `  F
) `  y ) J ( ( 1st `  G ) `  y
) ) ( ( x  e.  B  |->  X ) `  y ) )
13147, 130sylib 188 . 2  |-  ( ph  ->  A. y  e.  B  ( U `  y ) ( ( ( 1st `  F ) `  y
) J ( ( 1st `  G ) `
 y ) ) ( ( x  e.  B  |->  X ) `  y ) )
132 fuciso.q . . 3  |-  Q  =  ( C FuncCat  D )
133 fucinv.i . . 3  |-  I  =  (Inv `  Q )
134132, 10, 85, 5, 16, 133, 4fucinv 13896 . 2  |-  ( ph  ->  ( U ( F I G ) ( x  e.  B  |->  X )  <->  ( U  e.  ( F N G )  /\  ( x  e.  B  |->  X )  e.  ( G N F )  /\  A. y  e.  B  ( U `  y )
( ( ( 1st `  F ) `  y
) J ( ( 1st `  G ) `
 y ) ) ( ( x  e.  B  |->  X ) `  y ) ) ) )
1351, 128, 131, 134mpbir3and 1135 1  |-  ( ph  ->  U ( F I G ) ( x  e.  B  |->  X ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1633    e. wcel 1701   A.wral 2577   _Vcvv 2822   <.cop 3677   class class class wbr 4060    e. cmpt 4114    X. cxp 4724   Rel wrel 4731   -->wf 5288   ` cfv 5292  (class class class)co 5900   1stc1st 6162   2ndc2nd 6163   X_cixp 6860   Basecbs 13195    Hom chom 13266  compcco 13267   Catccat 13615   Idccid 13616  Sectcsect 13696  Invcinv 13697    Func cfunc 13777   Nat cnat 13864   FuncCat cfuc 13865
This theorem is referenced by:  fuciso  13898  yonedainv  14104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-oadd 6525  df-er 6702  df-map 6817  df-ixp 6861  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-2 9849  df-3 9850  df-4 9851  df-5 9852  df-6 9853  df-7 9854  df-8 9855  df-9 9856  df-10 9857  df-n0 10013  df-z 10072  df-dec 10172  df-uz 10278  df-fz 10830  df-struct 13197  df-ndx 13198  df-slot 13199  df-base 13200  df-hom 13279  df-cco 13280  df-cat 13619  df-cid 13620  df-sect 13699  df-inv 13700  df-func 13781  df-nat 13866  df-fuc 13867
  Copyright terms: Public domain W3C validator