Metamath Proof Explorer

Theorem fuccocl

Description: The composition of two natural transformations is a natural transformation. Remark 6.14(a) in Adamek p. 87. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fuccocl.q 
|- Q = ( C FuncCat D )
fuccocl.n 
|- N = ( C Nat D )
fuccocl.x 
|- .xb = ( comp ` Q )
fuccocl.r 
|- ( ph -> R e. ( F N G ) )
fuccocl.s 
|- ( ph -> S e. ( G N H ) )
Assertion fuccocl 
|- ( ph -> ( S ( <. F , G >. .xb H ) R ) e. ( F N H ) )

Proof

Step Hyp Ref Expression
1 fuccocl.q 
 |-  Q = ( C FuncCat D )
2 fuccocl.n 
 |-  N = ( C Nat D )
3 fuccocl.x 
 |-  .xb = ( comp ` Q )
4 fuccocl.r 
 |-  ( ph -> R e. ( F N G ) )
5 fuccocl.s 
 |-  ( ph -> S e. ( G N H ) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( comp ` D ) = ( comp ` D )
8 1 2 6 7 3 4 5 fucco 
 |-  ( ph -> ( S ( <. F , G >. .xb H ) R ) = ( x e. ( Base ` C ) |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
9 eqid 
 |-  ( Base ` D ) = ( Base ` D )
10 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
11 2 natrcl 
 |-  ( R e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
12 4 11 syl 
 |-  ( ph -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
13 12 simpld 
 |-  ( ph -> F e. ( C Func D ) )
14 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
15 13 14 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
16 15 simprd 
 |-  ( ph -> D e. Cat )
17 16 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
18 relfunc 
 |-  Rel ( C Func D )
19 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
20 18 13 19 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
21 6 9 20 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
22 21 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
23 2 natrcl 
 |-  ( S e. ( G N H ) -> ( G e. ( C Func D ) /\ H e. ( C Func D ) ) )
24 5 23 syl 
 |-  ( ph -> ( G e. ( C Func D ) /\ H e. ( C Func D ) ) )
25 24 simpld 
 |-  ( ph -> G e. ( C Func D ) )
26 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
27 18 25 26 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
28 6 9 27 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
29 28 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
30 24 simprd 
 |-  ( ph -> H e. ( C Func D ) )
31 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ H e. ( C Func D ) ) -> ( 1st ` H ) ( C Func D ) ( 2nd ` H ) )
32 18 30 31 sylancr 
 |-  ( ph -> ( 1st ` H ) ( C Func D ) ( 2nd ` H ) )
33 6 9 32 funcf1 
 |-  ( ph -> ( 1st ` H ) : ( Base ` C ) --> ( Base ` D ) )
34 33 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` H ) ` x ) e. ( Base ` D ) )
35 2 4 nat1st2nd 
 |-  ( ph -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
36 35 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
37 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
38 2 36 6 10 37 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( R ` x ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` x ) ) )
39 2 5 nat1st2nd 
 |-  ( ph -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. N <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
40 39 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. N <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
41 2 40 6 10 37 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( S ` x ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
42 9 10 7 17 22 29 34 38 41 catcocl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
43 42 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` C ) ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
44 fvex 
 |-  ( Base ` C ) e. _V
45 mptelixpg 
 |-  ( ( Base ` C ) e. _V -> ( ( x e. ( Base ` C ) |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) <-> A. x e. ( Base ` C ) ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) ) )
46 44 45 ax-mp 
 |-  ( ( x e. ( Base ` C ) |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) <-> A. x e. ( Base ` C ) ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
47 43 46 sylibr 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
48 8 47 eqeltrd 
 |-  ( ph -> ( S ( <. F , G >. .xb H ) R ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
49 16 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> D e. Cat )
50 21 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
51 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> x e. ( Base ` C ) )
52 50 51 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
53 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> y e. ( Base ` C ) )
54 50 53 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
55 28 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
56 55 53 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( 1st ` G ) ` y ) e. ( Base ` D ) )
57 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
58 20 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
59 6 57 10 58 51 53 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
60 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> f e. ( x ( Hom ` C ) y ) )
61 59 60 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
62 35 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
63 2 62 6 10 53 natcl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( R ` y ) e. ( ( ( 1st ` F ) ` y ) ( Hom ` D ) ( ( 1st ` G ) ` y ) ) )
64 33 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( 1st ` H ) : ( Base ` C ) --> ( Base ` D ) )
65 64 53 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( 1st ` H ) ` y ) e. ( Base ` D ) )
66 39 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. N <. ( 1st ` H ) , ( 2nd ` H ) >. ) )
67 2 66 6 10 53 natcl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( S ` y ) e. ( ( ( 1st ` G ) ` y ) ( Hom ` D ) ( ( 1st ` H ) ` y ) ) )
68 9 10 7 49 52 54 56 61 63 65 67 catass 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( S ` y ) ( <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` y ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( S ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( R ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` G ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) ) )
69 2 62 6 57 7 51 53 60 nati 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( R ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` G ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` G ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` y ) ) ( R ` x ) ) )
70 69 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( S ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( R ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` G ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) ) = ( ( S ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( ( x ( 2nd ` G ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` y ) ) ( R ` x ) ) ) )
71 55 51 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
72 2 62 6 10 51 natcl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( R ` x ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` x ) ) )
73 27 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
74 6 57 10 73 51 53 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( x ( 2nd ` G ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` y ) ) )
75 74 60 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( x ( 2nd ` G ) y ) ` f ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` y ) ) )
76 9 10 7 49 52 71 56 72 75 65 67 catass 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( S ` y ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` x ) ) = ( ( S ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( ( x ( 2nd ` G ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` G ) ` y ) ) ( R ` x ) ) ) )
77 2 66 6 57 7 51 53 60 nati 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( S ` y ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) = ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( S ` x ) ) )
78 77 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( S ` y ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` G ) y ) ` f ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` x ) ) = ( ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( S ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` x ) ) )
79 70 76 78 3eqtr2d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( S ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( R ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` G ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) ) = ( ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( S ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` x ) ) )
80 64 51 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( 1st ` H ) ` x ) e. ( Base ` D ) )
81 2 66 6 10 51 natcl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( S ` x ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) )
82 32 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( 1st ` H ) ( C Func D ) ( 2nd ` H ) )
83 6 57 10 82 51 53 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( x ( 2nd ` H ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` H ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` y ) ) )
84 83 60 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( x ( 2nd ` H ) y ) ` f ) e. ( ( ( 1st ` H ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` y ) ) )
85 9 10 7 49 52 71 80 72 81 65 84 catass 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( S ` x ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` x ) ) = ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
86 68 79 85 3eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( S ` y ) ( <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` y ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
87 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> R e. ( F N G ) )
88 5 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> S e. ( G N H ) )
89 1 2 6 7 3 87 88 53 fuccoval 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( S ( <. F , G >. .xb H ) R ) ` y ) = ( ( S ` y ) ( <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` y ) ) )
90 89 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( S ( <. F , G >. .xb H ) R ) ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( S ` y ) ( <. ( ( 1st ` F ) ` y ) , ( ( 1st ` G ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( R ` y ) ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) )
91 1 2 6 7 3 87 88 51 fuccoval 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( S ( <. F , G >. .xb H ) R ) ` x ) = ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) )
92 91 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( S ( <. F , G >. .xb H ) R ) ` x ) ) = ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( S ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` x ) ) ( R ` x ) ) ) )
93 86 90 92 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) -> ( ( ( S ( <. F , G >. .xb H ) R ) ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( S ( <. F , G >. .xb H ) R ) ` x ) ) )
94 93 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) ( ( ( S ( <. F , G >. .xb H ) R ) ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( S ( <. F , G >. .xb H ) R ) ` x ) ) )
95 2 6 57 10 7 13 30 isnat2 
 |-  ( ph -> ( ( S ( <. F , G >. .xb H ) R ) e. ( F N H ) <-> ( ( S ( <. F , G >. .xb H ) R ) e. X_ x e. ( Base ` C ) ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` H ) ` x ) ) /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) ( ( ( S ( <. F , G >. .xb H ) R ) ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( ( x ( 2nd ` H ) y ) ` f ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` H ) ` x ) >. ( comp ` D ) ( ( 1st ` H ) ` y ) ) ( ( S ( <. F , G >. .xb H ) R ) ` x ) ) ) ) )
96 48 94 95 mpbir2and 
 |-  ( ph -> ( S ( <. F , G >. .xb H ) R ) e. ( F N H ) )