Metamath Proof Explorer

Theorem funcres

Description: A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses funcres.f 
|- ( ph -> F e. ( C Func D ) )
funcres.h 
|- ( ph -> H e. ( Subcat ` C ) )
Assertion funcres 
|- ( ph -> ( F |`f H ) e. ( ( C |`cat H ) Func D ) )

Proof

Step Hyp Ref Expression
1 funcres.f 
 |-  ( ph -> F e. ( C Func D ) )
2 funcres.h 
 |-  ( ph -> H e. ( Subcat ` C ) )
3 1 2 resfval 
 |-  ( ph -> ( F |`f H ) = <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. )
4 3 fveq2d 
 |-  ( ph -> ( 2nd ` ( F |`f H ) ) = ( 2nd ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) )
5 fvex 
 |-  ( 1st ` F ) e. _V
6 5 resex 
 |-  ( ( 1st ` F ) |` dom dom H ) e. _V
7 dmexg 
 |-  ( H e. ( Subcat ` C ) -> dom H e. _V )
8 mptexg 
 |-  ( dom H e. _V -> ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V )
9 2 7 8 3syl 
 |-  ( ph -> ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V )
10 op2ndg 
 |-  ( ( ( ( 1st ` F ) |` dom dom H ) e. _V /\ ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) e. _V ) -> ( 2nd ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) = ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) )
11 6 9 10 sylancr 
 |-  ( ph -> ( 2nd ` <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. ) = ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) )
12 4 11 eqtrd 
 |-  ( ph -> ( 2nd ` ( F |`f H ) ) = ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) )
13 12 opeq2d 
 |-  ( ph -> <. ( ( 1st ` F ) |` dom dom H ) , ( 2nd ` ( F |`f H ) ) >. = <. ( ( 1st ` F ) |` dom dom H ) , ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) >. )
14 3 13 eqtr4d 
 |-  ( ph -> ( F |`f H ) = <. ( ( 1st ` F ) |` dom dom H ) , ( 2nd ` ( F |`f H ) ) >. )
15 eqid 
 |-  ( Base ` ( C |`cat H ) ) = ( Base ` ( C |`cat H ) )
16 eqid 
 |-  ( Base ` D ) = ( Base ` D )
17 eqid 
 |-  ( Hom ` ( C |`cat H ) ) = ( Hom ` ( C |`cat H ) )
18 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
19 eqid 
 |-  ( Id ` ( C |`cat H ) ) = ( Id ` ( C |`cat H ) )
20 eqid 
 |-  ( Id ` D ) = ( Id ` D )
21 eqid 
 |-  ( comp ` ( C |`cat H ) ) = ( comp ` ( C |`cat H ) )
22 eqid 
 |-  ( comp ` D ) = ( comp ` D )
23 eqid 
 |-  ( C |`cat H ) = ( C |`cat H )
24 23 2 subccat 
 |-  ( ph -> ( C |`cat H ) e. Cat )
25 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
26 1 25 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
27 26 simprd 
 |-  ( ph -> D e. Cat )
28 eqid 
 |-  ( Base ` C ) = ( Base ` C )
29 relfunc 
 |-  Rel ( C Func D )
30 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
31 29 1 30 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
32 28 16 31 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
33 eqidd 
 |-  ( ph -> dom dom H = dom dom H )
34 2 33 subcfn 
 |-  ( ph -> H Fn ( dom dom H X. dom dom H ) )
35 2 34 28 subcss1 
 |-  ( ph -> dom dom H C_ ( Base ` C ) )
36 32 35 fssresd 
 |-  ( ph -> ( ( 1st ` F ) |` dom dom H ) : dom dom H --> ( Base ` D ) )
37 26 simpld 
 |-  ( ph -> C e. Cat )
38 23 28 37 34 35 rescbas 
 |-  ( ph -> dom dom H = ( Base ` ( C |`cat H ) ) )
39 38 feq2d 
 |-  ( ph -> ( ( ( 1st ` F ) |` dom dom H ) : dom dom H --> ( Base ` D ) <-> ( ( 1st ` F ) |` dom dom H ) : ( Base ` ( C |`cat H ) ) --> ( Base ` D ) ) )
40 36 39 mpbid 
 |-  ( ph -> ( ( 1st ` F ) |` dom dom H ) : ( Base ` ( C |`cat H ) ) --> ( Base ` D ) )
41 fvex 
 |-  ( ( 2nd ` F ) ` z ) e. _V
42 41 resex 
 |-  ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) e. _V
43 eqid 
 |-  ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) = ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) )
44 42 43 fnmpti 
 |-  ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) Fn dom H
45 12 eqcomd 
 |-  ( ph -> ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) = ( 2nd ` ( F |`f H ) ) )
46 fndm 
 |-  ( H Fn ( dom dom H X. dom dom H ) -> dom H = ( dom dom H X. dom dom H ) )
47 34 46 syl 
 |-  ( ph -> dom H = ( dom dom H X. dom dom H ) )
48 38 sqxpeqd 
 |-  ( ph -> ( dom dom H X. dom dom H ) = ( ( Base ` ( C |`cat H ) ) X. ( Base ` ( C |`cat H ) ) ) )
49 47 48 eqtrd 
 |-  ( ph -> dom H = ( ( Base ` ( C |`cat H ) ) X. ( Base ` ( C |`cat H ) ) ) )
50 45 49 fneq12d 
 |-  ( ph -> ( ( z e. dom H |-> ( ( ( 2nd ` F ) ` z ) |` ( H ` z ) ) ) Fn dom H <-> ( 2nd ` ( F |`f H ) ) Fn ( ( Base ` ( C |`cat H ) ) X. ( Base ` ( C |`cat H ) ) ) ) )
51 44 50 mpbii 
 |-  ( ph -> ( 2nd ` ( F |`f H ) ) Fn ( ( Base ` ( C |`cat H ) ) X. ( Base ` ( C |`cat H ) ) ) )
52 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
53 31 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
54 35 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> dom dom H C_ ( Base ` C ) )
55 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> x e. ( Base ` ( C |`cat H ) ) )
56 38 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> dom dom H = ( Base ` ( C |`cat H ) ) )
57 55 56 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> x e. dom dom H )
58 54 57 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> x e. ( Base ` C ) )
59 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> y e. ( Base ` ( C |`cat H ) ) )
60 59 56 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> y e. dom dom H )
61 54 60 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> y e. ( Base ` C ) )
62 28 52 18 53 58 61 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
63 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> H e. ( Subcat ` C ) )
64 34 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> H Fn ( dom dom H X. dom dom H ) )
65 63 64 52 57 60 subcss2 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( x H y ) C_ ( x ( Hom ` C ) y ) )
66 62 65 fssresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( ( x ( 2nd ` F ) y ) |` ( x H y ) ) : ( x H y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
67 1 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> F e. ( C Func D ) )
68 67 63 64 57 60 resf2nd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( x ( 2nd ` ( F |`f H ) ) y ) = ( ( x ( 2nd ` F ) y ) |` ( x H y ) ) )
69 68 feq1d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( ( x ( 2nd ` ( F |`f H ) ) y ) : ( x H y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) <-> ( ( x ( 2nd ` F ) y ) |` ( x H y ) ) : ( x H y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) ) )
70 66 69 mpbird 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( x ( 2nd ` ( F |`f H ) ) y ) : ( x H y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
71 23 28 37 34 35 reschom 
 |-  ( ph -> H = ( Hom ` ( C |`cat H ) ) )
72 71 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> H = ( Hom ` ( C |`cat H ) ) )
73 72 oveqd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( x H y ) = ( x ( Hom ` ( C |`cat H ) ) y ) )
74 57 fvresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( ( ( 1st ` F ) |` dom dom H ) ` x ) = ( ( 1st ` F ) ` x ) )
75 60 fvresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( ( ( 1st ` F ) |` dom dom H ) ` y ) = ( ( 1st ` F ) ` y ) )
76 74 75 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( ( ( ( 1st ` F ) |` dom dom H ) ` x ) ( Hom ` D ) ( ( ( 1st ` F ) |` dom dom H ) ` y ) ) = ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
77 76 eqcomd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) = ( ( ( ( 1st ` F ) |` dom dom H ) ` x ) ( Hom ` D ) ( ( ( 1st ` F ) |` dom dom H ) ` y ) ) )
78 73 77 feq23d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( ( x ( 2nd ` ( F |`f H ) ) y ) : ( x H y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) <-> ( x ( 2nd ` ( F |`f H ) ) y ) : ( x ( Hom ` ( C |`cat H ) ) y ) --> ( ( ( ( 1st ` F ) |` dom dom H ) ` x ) ( Hom ` D ) ( ( ( 1st ` F ) |` dom dom H ) ` y ) ) ) )
79 70 78 mpbid 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) ) ) -> ( x ( 2nd ` ( F |`f H ) ) y ) : ( x ( Hom ` ( C |`cat H ) ) y ) --> ( ( ( ( 1st ` F ) |` dom dom H ) ` x ) ( Hom ` D ) ( ( ( 1st ` F ) |` dom dom H ) ` y ) ) )
80 1 adantr 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> F e. ( C Func D ) )
81 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> H e. ( Subcat ` C ) )
82 34 adantr 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> H Fn ( dom dom H X. dom dom H ) )
83 38 eleq2d 
 |-  ( ph -> ( x e. dom dom H <-> x e. ( Base ` ( C |`cat H ) ) ) )
84 83 biimpar 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> x e. dom dom H )
85 80 81 82 84 84 resf2nd 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( x ( 2nd ` ( F |`f H ) ) x ) = ( ( x ( 2nd ` F ) x ) |` ( x H x ) ) )
86 eqid 
 |-  ( Id ` C ) = ( Id ` C )
87 23 81 82 86 84 subcid 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( Id ` C ) ` x ) = ( ( Id ` ( C |`cat H ) ) ` x ) )
88 87 eqcomd 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( Id ` ( C |`cat H ) ) ` x ) = ( ( Id ` C ) ` x ) )
89 85 88 fveq12d 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( x ( 2nd ` ( F |`f H ) ) x ) ` ( ( Id ` ( C |`cat H ) ) ` x ) ) = ( ( ( x ( 2nd ` F ) x ) |` ( x H x ) ) ` ( ( Id ` C ) ` x ) ) )
90 31 adantr 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
91 38 35 eqsstrrd 
 |-  ( ph -> ( Base ` ( C |`cat H ) ) C_ ( Base ` C ) )
92 91 sselda 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> x e. ( Base ` C ) )
93 28 86 20 90 92 funcid 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) )
94 81 82 84 86 subcidcl 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( Id ` C ) ` x ) e. ( x H x ) )
95 94 fvresd 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( ( x ( 2nd ` F ) x ) |` ( x H x ) ) ` ( ( Id ` C ) ` x ) ) = ( ( x ( 2nd ` F ) x ) ` ( ( Id ` C ) ` x ) ) )
96 84 fvresd 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( ( 1st ` F ) |` dom dom H ) ` x ) = ( ( 1st ` F ) ` x ) )
97 96 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( Id ` D ) ` ( ( ( 1st ` F ) |` dom dom H ) ` x ) ) = ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) )
98 93 95 97 3eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( ( x ( 2nd ` F ) x ) |` ( x H x ) ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( ( ( 1st ` F ) |` dom dom H ) ` x ) ) )
99 89 98 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` ( C |`cat H ) ) ) -> ( ( x ( 2nd ` ( F |`f H ) ) x ) ` ( ( Id ` ( C |`cat H ) ) ` x ) ) = ( ( Id ` D ) ` ( ( ( 1st ` F ) |` dom dom H ) ` x ) ) )
100 2 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> H e. ( Subcat ` C ) )
101 34 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> H Fn ( dom dom H X. dom dom H ) )
102 simp21 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> x e. ( Base ` ( C |`cat H ) ) )
103 38 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> dom dom H = ( Base ` ( C |`cat H ) ) )
104 102 103 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> x e. dom dom H )
105 eqid 
 |-  ( comp ` C ) = ( comp ` C )
106 simp22 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> y e. ( Base ` ( C |`cat H ) ) )
107 106 103 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> y e. dom dom H )
108 simp23 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> z e. ( Base ` ( C |`cat H ) ) )
109 108 103 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> z e. dom dom H )
110 simp3l 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> f e. ( x ( Hom ` ( C |`cat H ) ) y ) )
111 71 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> H = ( Hom ` ( C |`cat H ) ) )
112 111 oveqd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( x H y ) = ( x ( Hom ` ( C |`cat H ) ) y ) )
113 110 112 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> f e. ( x H y ) )
114 simp3r 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> g e. ( y ( Hom ` ( C |`cat H ) ) z ) )
115 111 oveqd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( y H z ) = ( y ( Hom ` ( C |`cat H ) ) z ) )
116 114 115 eleqtrrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> g e. ( y H z ) )
117 100 101 104 105 107 109 113 116 subccocl 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x H z ) )
118 117 fvresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( ( x ( 2nd ` F ) z ) |` ( x H z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) )
119 31 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
120 35 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> dom dom H C_ ( Base ` C ) )
121 120 104 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> x e. ( Base ` C ) )
122 120 107 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> y e. ( Base ` C ) )
123 120 109 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> z e. ( Base ` C ) )
124 100 101 52 104 107 subcss2 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( x H y ) C_ ( x ( Hom ` C ) y ) )
125 124 113 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> f e. ( x ( Hom ` C ) y ) )
126 100 101 52 107 109 subcss2 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( y H z ) C_ ( y ( Hom ` C ) z ) )
127 126 116 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> g e. ( y ( Hom ` C ) z ) )
128 28 52 105 22 119 121 122 123 125 127 funcco 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( x ( 2nd ` F ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) )
129 118 128 eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( ( x ( 2nd ` F ) z ) |` ( x H z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) )
130 1 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> F e. ( C Func D ) )
131 130 100 101 104 109 resf2nd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( x ( 2nd ` ( F |`f H ) ) z ) = ( ( x ( 2nd ` F ) z ) |` ( x H z ) ) )
132 23 28 37 34 35 105 rescco 
 |-  ( ph -> ( comp ` C ) = ( comp ` ( C |`cat H ) ) )
133 132 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( comp ` C ) = ( comp ` ( C |`cat H ) ) )
134 133 eqcomd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( comp ` ( C |`cat H ) ) = ( comp ` C ) )
135 134 oveqd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( <. x , y >. ( comp ` ( C |`cat H ) ) z ) = ( <. x , y >. ( comp ` C ) z ) )
136 135 oveqd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( g ( <. x , y >. ( comp ` ( C |`cat H ) ) z ) f ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) )
137 131 136 fveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( x ( 2nd ` ( F |`f H ) ) z ) ` ( g ( <. x , y >. ( comp ` ( C |`cat H ) ) z ) f ) ) = ( ( ( x ( 2nd ` F ) z ) |` ( x H z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) )
138 104 fvresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( ( 1st ` F ) |` dom dom H ) ` x ) = ( ( 1st ` F ) ` x ) )
139 107 fvresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( ( 1st ` F ) |` dom dom H ) ` y ) = ( ( 1st ` F ) ` y ) )
140 138 139 opeq12d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> <. ( ( ( 1st ` F ) |` dom dom H ) ` x ) , ( ( ( 1st ` F ) |` dom dom H ) ` y ) >. = <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. )
141 109 fvresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( ( 1st ` F ) |` dom dom H ) ` z ) = ( ( 1st ` F ) ` z ) )
142 140 141 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( <. ( ( ( 1st ` F ) |` dom dom H ) ` x ) , ( ( ( 1st ` F ) |` dom dom H ) ` y ) >. ( comp ` D ) ( ( ( 1st ` F ) |` dom dom H ) ` z ) ) = ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) )
143 130 100 101 107 109 resf2nd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( y ( 2nd ` ( F |`f H ) ) z ) = ( ( y ( 2nd ` F ) z ) |` ( y H z ) ) )
144 143 fveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( y ( 2nd ` ( F |`f H ) ) z ) ` g ) = ( ( ( y ( 2nd ` F ) z ) |` ( y H z ) ) ` g ) )
145 116 fvresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( ( y ( 2nd ` F ) z ) |` ( y H z ) ) ` g ) = ( ( y ( 2nd ` F ) z ) ` g ) )
146 144 145 eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( y ( 2nd ` ( F |`f H ) ) z ) ` g ) = ( ( y ( 2nd ` F ) z ) ` g ) )
147 130 100 101 104 107 resf2nd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( x ( 2nd ` ( F |`f H ) ) y ) = ( ( x ( 2nd ` F ) y ) |` ( x H y ) ) )
148 147 fveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( x ( 2nd ` ( F |`f H ) ) y ) ` f ) = ( ( ( x ( 2nd ` F ) y ) |` ( x H y ) ) ` f ) )
149 113 fvresd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( ( x ( 2nd ` F ) y ) |` ( x H y ) ) ` f ) = ( ( x ( 2nd ` F ) y ) ` f ) )
150 148 149 eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( x ( 2nd ` ( F |`f H ) ) y ) ` f ) = ( ( x ( 2nd ` F ) y ) ` f ) )
151 142 146 150 oveq123d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( ( y ( 2nd ` ( F |`f H ) ) z ) ` g ) ( <. ( ( ( 1st ` F ) |` dom dom H ) ` x ) , ( ( ( 1st ` F ) |` dom dom H ) ` y ) >. ( comp ` D ) ( ( ( 1st ` F ) |` dom dom H ) ` z ) ) ( ( x ( 2nd ` ( F |`f H ) ) y ) ` f ) ) = ( ( ( y ( 2nd ` F ) z ) ` g ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. ( comp ` D ) ( ( 1st ` F ) ` z ) ) ( ( x ( 2nd ` F ) y ) ` f ) ) )
152 129 137 151 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` ( C |`cat H ) ) /\ y e. ( Base ` ( C |`cat H ) ) /\ z e. ( Base ` ( C |`cat H ) ) ) /\ ( f e. ( x ( Hom ` ( C |`cat H ) ) y ) /\ g e. ( y ( Hom ` ( C |`cat H ) ) z ) ) ) -> ( ( x ( 2nd ` ( F |`f H ) ) z ) ` ( g ( <. x , y >. ( comp ` ( C |`cat H ) ) z ) f ) ) = ( ( ( y ( 2nd ` ( F |`f H ) ) z ) ` g ) ( <. ( ( ( 1st ` F ) |` dom dom H ) ` x ) , ( ( ( 1st ` F ) |` dom dom H ) ` y ) >. ( comp ` D ) ( ( ( 1st ` F ) |` dom dom H ) ` z ) ) ( ( x ( 2nd ` ( F |`f H ) ) y ) ` f ) ) )
153 15 16 17 18 19 20 21 22 24 27 40 51 79 99 152 isfuncd 
 |-  ( ph -> ( ( 1st ` F ) |` dom dom H ) ( ( C |`cat H ) Func D ) ( 2nd ` ( F |`f H ) ) )
154 df-br 
 |-  ( ( ( 1st ` F ) |` dom dom H ) ( ( C |`cat H ) Func D ) ( 2nd ` ( F |`f H ) ) <-> <. ( ( 1st ` F ) |` dom dom H ) , ( 2nd ` ( F |`f H ) ) >. e. ( ( C |`cat H ) Func D ) )
155 153 154 sylib 
 |-  ( ph -> <. ( ( 1st ` F ) |` dom dom H ) , ( 2nd ` ( F |`f H ) ) >. e. ( ( C |`cat H ) Func D ) )
156 14 155 eqeltrd 
 |-  ( ph -> ( F |`f H ) e. ( ( C |`cat H ) Func D ) )