Metamath Proof Explorer

Theorem invfuc

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)

Ref Expression
Hypotheses 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 invfuc 
|- ( ph -> U ( F I G ) ( x e. B |-> X ) )

Proof

Step Hyp Ref Expression
1 fuciso.q 
 |-  Q = ( C FuncCat D )
2 fuciso.b 
 |-  B = ( Base ` C )
3 fuciso.n 
 |-  N = ( C Nat D )
4 fuciso.f 
 |-  ( ph -> F e. ( C Func D ) )
5 fuciso.g 
 |-  ( ph -> G e. ( C Func D ) )
6 fucinv.i 
 |-  I = ( Inv ` Q )
7 fucinv.j 
 |-  J = ( Inv ` D )
8 invfuc.u 
 |-  ( ph -> U e. ( F N G ) )
9 invfuc.v 
 |-  ( ( ph /\ x e. B ) -> ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) X )
10 eqid 
 |-  ( Base ` D ) = ( Base ` D )
11 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
12 4 11 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
13 12 simprd 
 |-  ( ph -> D e. Cat )
14 13 adantr 
 |-  ( ( ph /\ x e. B ) -> D e. Cat )
15 relfunc 
 |-  Rel ( C Func D )
16 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
17 15 4 16 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
18 2 10 17 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` D ) )
19 18 ffvelrnda 
 |-  ( ( ph /\ x e. B ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
20 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
21 15 5 20 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
22 2 10 21 funcf1 
 |-  ( ph -> ( 1st ` G ) : B --> ( Base ` D ) )
23 22 ffvelrnda 
 |-  ( ( ph /\ x e. B ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
24 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
25 10 7 14 19 23 24 invss 
 |-  ( ( 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 ) ) ) )
26 25 ssbrd 
 |-  ( ( 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 ) )
27 9 26 mpd 
 |-  ( ( ph /\ x e. B ) -> ( U ` x ) ( ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` x ) ) X. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) ) X )
28 brxp 
 |-  ( ( 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 ) ) ) )
29 28 simprbi 
 |-  ( ( 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 ) ) )
30 27 29 syl 
 |-  ( ( ph /\ x e. B ) -> X e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
31 30 ralrimiva 
 |-  ( ph -> A. x e. B X e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
32 2 fvexi 
 |-  B e. _V
33 mptelixpg 
 |-  ( 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 ) ) ) )
34 32 33 ax-mp 
 |-  ( ( 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 ) ) )
35 31 34 sylibr 
 |-  ( ph -> ( x e. B |-> X ) e. X_ x e. B ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
36 fveq2 
 |-  ( x = y -> ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` y ) )
37 fveq2 
 |-  ( x = y -> ( ( 1st ` F ) ` x ) = ( ( 1st ` F ) ` y ) )
38 36 37 oveq12d 
 |-  ( x = y -> ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) = ( ( ( 1st ` G ) ` y ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
39 38 cbvixpv 
 |-  X_ x e. B ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) = X_ y e. B ( ( ( 1st ` G ) ` y ) ( Hom ` D ) ( ( 1st ` F ) ` y ) )
40 35 39 eleqtrdi 
 |-  ( ph -> ( x e. B |-> X ) e. X_ y e. B ( ( ( 1st ` G ) ` y ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
41 simpr2 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> z e. B )
42 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
43 eqid 
 |-  ( x e. B |-> X ) = ( x e. B |-> X )
44 43 fvmpt2 
 |-  ( ( x e. B /\ X e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) ) -> ( ( x e. B |-> X ) ` x ) = X )
45 42 30 44 syl2anc 
 |-  ( ( ph /\ x e. B ) -> ( ( x e. B |-> X ) ` x ) = X )
46 9 45 breqtrrd 
 |-  ( ( ph /\ x e. B ) -> ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( ( x e. B |-> X ) ` x ) )
47 46 ralrimiva 
 |-  ( ph -> A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( ( x e. B |-> X ) ` x ) )
48 47 adantr 
 |-  ( ( 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 
 |-  F/_ x ( U ` z )
50 nfcv 
 |-  F/_ x ( ( ( 1st ` F ) ` z ) J ( ( 1st ` G ) ` z ) )
51 nffvmpt1 
 |-  F/_ x ( ( x e. B |-> X ) ` z )
52 49 50 51 nfbr 
 |-  F/ x ( U ` z ) ( ( ( 1st ` F ) ` z ) J ( ( 1st ` G ) ` z ) ) ( ( x e. B |-> X ) ` z )
53 fveq2 
 |-  ( x = z -> ( U ` x ) = ( U ` z ) )
54 fveq2 
 |-  ( x = z -> ( ( 1st ` F ) ` x ) = ( ( 1st ` F ) ` z ) )
55 fveq2 
 |-  ( x = z -> ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` z ) )
56 54 55 oveq12d 
 |-  ( x = z -> ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) = ( ( ( 1st ` F ) ` z ) J ( ( 1st ` G ) ` z ) ) )
57 fveq2 
 |-  ( x = z -> ( ( x e. B |-> X ) ` x ) = ( ( x e. B |-> X ) ` z ) )
58 53 56 57 breq123d 
 |-  ( 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 ) ) )
59 52 58 rspc 
 |-  ( 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 ) ) )
60 41 48 59 sylc 
 |-  ( ( 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 ) )
61 13 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> D e. Cat )
62 18 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( 1st ` F ) : B --> ( Base ` D ) )
63 62 41 ffvelrnd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` F ) ` z ) e. ( Base ` D ) )
64 22 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( 1st ` G ) : B --> ( Base ` D ) )
65 64 41 ffvelrnd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` G ) ` z ) e. ( Base ` D ) )
66 eqid 
 |-  ( Sect ` D ) = ( Sect ` D )
67 10 7 61 63 65 66 isinv 
 |-  ( ( 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 ) ) ) )
68 60 67 mpbid 
 |-  ( ( 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 ) ) )
69 68 simpld 
 |-  ( ( 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 
 |-  ( comp ` D ) = ( comp ` D )
71 eqid 
 |-  ( Id ` D ) = ( Id ` D )
72 10 24 70 71 66 61 63 65 issect 
 |-  ( ( 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 ) ) ) ) )
73 69 72 mpbid 
 |-  ( ( 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 ) ) ) )
74 73 simp3d 
 |-  ( ( 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 ) ) )
75 74 oveq1d 
 |-  ( ( 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 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> y e. B )
77 62 76 ffvelrnd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
78 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
79 17 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
80 2 78 24 79 76 41 funcf2 
 |-  ( ( 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 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> f e. ( y ( Hom ` C ) z ) )
82 80 81 ffvelrnd 
 |-  ( ( 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 ) ) )
83 10 24 71 61 77 70 63 82 catlid 
 |-  ( ( 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 ) )
84 75 83 eqtr2d 
 |-  ( ( 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 8 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> U e. ( F N G ) )
86 3 85 nat1st2nd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> U e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
87 3 86 2 24 41 natcl 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( U ` z ) e. ( ( ( 1st ` F ) ` z ) ( Hom ` D ) ( ( 1st ` G ) ` z ) ) )
88 73 simp2d 
 |-  ( ( 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 ) ) )
89 10 24 70 61 77 63 65 82 87 63 88 catass 
 |-  ( ( 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 ) ) ) )
90 3 86 2 78 70 76 41 81 nati 
 |-  ( ( 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 ) ) )
91 90 oveq2d 
 |-  ( ( 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 ) ) ) )
92 84 89 91 3eqtrd 
 |-  ( ( 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 ) ) ) )
93 92 oveq1d 
 |-  ( ( 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 ) ) )
94 64 76 ffvelrnd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( ( 1st ` G ) ` y ) e. ( Base ` D ) )
95 nfcv 
 |-  F/_ x ( U ` y )
96 nfcv 
 |-  F/_ x ( ( ( 1st ` F ) ` y ) J ( ( 1st ` G ) ` y ) )
97 nffvmpt1 
 |-  F/_ x ( ( x e. B |-> X ) ` y )
98 95 96 97 nfbr 
 |-  F/ x ( U ` y ) ( ( ( 1st ` F ) ` y ) J ( ( 1st ` G ) ` y ) ) ( ( x e. B |-> X ) ` y )
99 fveq2 
 |-  ( x = y -> ( U ` x ) = ( U ` y ) )
100 37 36 oveq12d 
 |-  ( x = y -> ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) = ( ( ( 1st ` F ) ` y ) J ( ( 1st ` G ) ` y ) ) )
101 fveq2 
 |-  ( x = y -> ( ( x e. B |-> X ) ` x ) = ( ( x e. B |-> X ) ` y ) )
102 99 100 101 breq123d 
 |-  ( 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 ) ) )
103 98 102 rspc 
 |-  ( 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 ) ) )
104 76 48 103 sylc 
 |-  ( ( 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 ) )
105 10 7 61 77 94 66 isinv 
 |-  ( ( 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 ) ) ) )
106 104 105 mpbid 
 |-  ( ( 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 ) ) )
107 106 simprd 
 |-  ( ( 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 ) )
108 10 24 70 71 66 61 94 77 issect 
 |-  ( ( 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 ) ) ) ) )
109 107 108 mpbid 
 |-  ( ( 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 ) ) ) )
110 109 simp1d 
 |-  ( ( 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 ) ) )
111 109 simp2d 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( U ` y ) e. ( ( ( 1st ` F ) ` y ) ( Hom ` D ) ( ( 1st ` G ) ` y ) ) )
112 21 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
113 2 78 24 112 76 41 funcf2 
 |-  ( ( 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 ) ) )
114 113 81 ffvelrnd 
 |-  ( ( 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 ) ) )
115 10 24 70 61 77 94 65 111 114 catcocl 
 |-  ( ( 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 ) ) )
116 10 24 70 61 94 77 65 110 115 63 88 catass 
 |-  ( ( 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 ) ) ) )
117 3 86 2 24 76 natcl 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ f e. ( y ( Hom ` C ) z ) ) ) -> ( U ` y ) e. ( ( ( 1st ` F ) ` y ) ( Hom ` D ) ( ( 1st ` G ) ` y ) ) )
118 10 24 70 61 94 77 94 110 117 65 114 catass 
 |-  ( ( 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 ) ) ) )
119 109 simp3d 
 |-  ( ( 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 ) ) )
120 119 oveq2d 
 |-  ( ( 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 ) ) ) )
121 10 24 71 61 94 70 65 114 catrid 
 |-  ( ( 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 ) )
122 118 120 121 3eqtrd 
 |-  ( ( 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 ) )
123 122 oveq2d 
 |-  ( ( 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 ) ) )
124 93 116 123 3eqtrrd 
 |-  ( ( 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 ) ) )
125 124 ralrimivvva 
 |-  ( 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 ) ) )
126 3 2 78 24 70 5 4 isnat2 
 |-  ( 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 ) ) ) ) )
127 40 125 126 mpbir2and 
 |-  ( ph -> ( x e. B |-> X ) e. ( G N F ) )
128 nfv 
 |-  F/ y ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( ( x e. B |-> X ) ` x )
129 128 98 102 cbvralw 
 |-  ( 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 ) )
130 47 129 sylib 
 |-  ( ph -> A. y e. B ( U ` y ) ( ( ( 1st ` F ) ` y ) J ( ( 1st ` G ) ` y ) ) ( ( x e. B |-> X ) ` y ) )
131 1 2 3 4 5 6 7 fucinv 
 |-  ( 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 ) ) ) )
132 8 127 130 131 mpbir3and 
 |-  ( ph -> U ( F I G ) ( x e. B |-> X ) )