Metamath Proof Explorer

Theorem yonedalem4c

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses yoneda.y 
|- Y = ( Yon ` C )
yoneda.b 
|- B = ( Base ` C )
yoneda.1 
|- .1. = ( Id ` C )
yoneda.o 
|- O = ( oppCat ` C )
yoneda.s 
|- S = ( SetCat ` U )
yoneda.t 
|- T = ( SetCat ` V )
yoneda.q 
|- Q = ( O FuncCat S )
yoneda.h 
|- H = ( HomF ` Q )
yoneda.r 
|- R = ( ( Q Xc. O ) FuncCat T )
yoneda.e 
|- E = ( O evalF S )
yoneda.z 
|- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
yoneda.c 
|- ( ph -> C e. Cat )
yoneda.w 
|- ( ph -> V e. W )
yoneda.u 
|- ( ph -> ran ( Homf ` C ) C_ U )
yoneda.v 
|- ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
yonedalem21.f 
|- ( ph -> F e. ( O Func S ) )
yonedalem21.x 
|- ( ph -> X e. B )
yonedalem4.n 
|- N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )
yonedalem4.p 
|- ( ph -> A e. ( ( 1st ` F ) ` X ) )
Assertion yonedalem4c 
|- ( ph -> ( ( F N X ) ` A ) e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )

Proof

Step Hyp Ref Expression
1 yoneda.y 
 |-  Y = ( Yon ` C )
2 yoneda.b 
 |-  B = ( Base ` C )
3 yoneda.1 
 |-  .1. = ( Id ` C )
4 yoneda.o 
 |-  O = ( oppCat ` C )
5 yoneda.s 
 |-  S = ( SetCat ` U )
6 yoneda.t 
 |-  T = ( SetCat ` V )
7 yoneda.q 
 |-  Q = ( O FuncCat S )
8 yoneda.h 
 |-  H = ( HomF ` Q )
9 yoneda.r 
 |-  R = ( ( Q Xc. O ) FuncCat T )
10 yoneda.e 
 |-  E = ( O evalF S )
11 yoneda.z 
 |-  Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
12 yoneda.c 
 |-  ( ph -> C e. Cat )
13 yoneda.w 
 |-  ( ph -> V e. W )
14 yoneda.u 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
15 yoneda.v 
 |-  ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
16 yonedalem21.f 
 |-  ( ph -> F e. ( O Func S ) )
17 yonedalem21.x 
 |-  ( ph -> X e. B )
18 yonedalem4.n 
 |-  N = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )
19 yonedalem4.p 
 |-  ( ph -> A e. ( ( 1st ` F ) ` X ) )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 yonedalem4a 
 |-  ( ph -> ( ( F N X ) ` A ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) )
21 oveq1 
 |-  ( y = z -> ( y ( Hom ` C ) X ) = ( z ( Hom ` C ) X ) )
22 oveq2 
 |-  ( y = z -> ( X ( 2nd ` F ) y ) = ( X ( 2nd ` F ) z ) )
23 22 fveq1d 
 |-  ( y = z -> ( ( X ( 2nd ` F ) y ) ` g ) = ( ( X ( 2nd ` F ) z ) ` g ) )
24 23 fveq1d 
 |-  ( y = z -> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) = ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) )
25 21 24 mpteq12dv 
 |-  ( y = z -> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) = ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) )
26 25 cbvmptv 
 |-  ( y e. B |-> ( g e. ( y ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) y ) ` g ) ` A ) ) ) = ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) )
27 20 26 eqtrdi 
 |-  ( ph -> ( ( F N X ) ` A ) = ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) ) )
28 4 2 oppcbas 
 |-  B = ( Base ` O )
29 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
30 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
31 relfunc 
 |-  Rel ( O Func S )
32 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ F e. ( O Func S ) ) -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
33 31 16 32 sylancr 
 |-  ( ph -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
34 33 adantr 
 |-  ( ( ph /\ z e. B ) -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
35 17 adantr 
 |-  ( ( ph /\ z e. B ) -> X e. B )
36 simpr 
 |-  ( ( ph /\ z e. B ) -> z e. B )
37 28 29 30 34 35 36 funcf2 
 |-  ( ( ph /\ z e. B ) -> ( X ( 2nd ` F ) z ) : ( X ( Hom ` O ) z ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
38 37 adantr 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> ( X ( 2nd ` F ) z ) : ( X ( Hom ` O ) z ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
39 simpr 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> g e. ( z ( Hom ` C ) X ) )
40 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
41 40 4 oppchom 
 |-  ( X ( Hom ` O ) z ) = ( z ( Hom ` C ) X )
42 39 41 eleqtrrdi 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> g e. ( X ( Hom ` O ) z ) )
43 38 42 ffvelrnd 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> ( ( X ( 2nd ` F ) z ) ` g ) e. ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
44 15 unssbd 
 |-  ( ph -> U C_ V )
45 13 44 ssexd 
 |-  ( ph -> U e. _V )
46 45 adantr 
 |-  ( ( ph /\ z e. B ) -> U e. _V )
47 46 adantr 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> U e. _V )
48 eqid 
 |-  ( Base ` S ) = ( Base ` S )
49 28 48 33 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` S ) )
50 5 45 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
51 50 feq3d 
 |-  ( ph -> ( ( 1st ` F ) : B --> U <-> ( 1st ` F ) : B --> ( Base ` S ) ) )
52 49 51 mpbird 
 |-  ( ph -> ( 1st ` F ) : B --> U )
53 52 17 ffvelrnd 
 |-  ( ph -> ( ( 1st ` F ) ` X ) e. U )
54 53 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> ( ( 1st ` F ) ` X ) e. U )
55 52 ffvelrnda 
 |-  ( ( ph /\ z e. B ) -> ( ( 1st ` F ) ` z ) e. U )
56 55 adantr 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> ( ( 1st ` F ) ` z ) e. U )
57 5 47 30 54 56 elsetchom 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> ( ( ( X ( 2nd ` F ) z ) ` g ) e. ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) <-> ( ( X ( 2nd ` F ) z ) ` g ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` z ) ) )
58 43 57 mpbid 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> ( ( X ( 2nd ` F ) z ) ` g ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` z ) )
59 19 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> A e. ( ( 1st ` F ) ` X ) )
60 58 59 ffvelrnd 
 |-  ( ( ( ph /\ z e. B ) /\ g e. ( z ( Hom ` C ) X ) ) -> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) e. ( ( 1st ` F ) ` z ) )
61 60 fmpttd 
 |-  ( ( ph /\ z e. B ) -> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) : ( z ( Hom ` C ) X ) --> ( ( 1st ` F ) ` z ) )
62 12 adantr 
 |-  ( ( ph /\ z e. B ) -> C e. Cat )
63 1 2 62 35 40 36 yon11 
 |-  ( ( ph /\ z e. B ) -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) = ( z ( Hom ` C ) X ) )
64 63 feq2d 
 |-  ( ( ph /\ z e. B ) -> ( ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) <-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) : ( z ( Hom ` C ) X ) --> ( ( 1st ` F ) ` z ) ) )
65 61 64 mpbird 
 |-  ( ( ph /\ z e. B ) -> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) )
66 1 2 12 17 4 5 45 14 yon1cl 
 |-  ( ph -> ( ( 1st ` Y ) ` X ) e. ( O Func S ) )
67 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ ( ( 1st ` Y ) ` X ) e. ( O Func S ) ) -> ( 1st ` ( ( 1st ` Y ) ` X ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` X ) ) )
68 31 66 67 sylancr 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` X ) ) )
69 28 48 68 funcf1 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> ( Base ` S ) )
70 50 feq3d 
 |-  ( ph -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> U <-> ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> ( Base ` S ) ) )
71 69 70 mpbird 
 |-  ( ph -> ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> U )
72 71 ffvelrnda 
 |-  ( ( ph /\ z e. B ) -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) e. U )
73 5 46 30 72 55 elsetchom 
 |-  ( ( ph /\ z e. B ) -> ( ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) <-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) ) )
74 65 73 mpbird 
 |-  ( ( ph /\ z e. B ) -> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
75 74 ralrimiva 
 |-  ( ph -> A. z e. B ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
76 2 fvexi 
 |-  B e. _V
77 mptelixpg 
 |-  ( B e. _V -> ( ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) ) e. X_ z e. B ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) <-> A. z e. B ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) ) )
78 76 77 ax-mp 
 |-  ( ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) ) e. X_ z e. B ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) <-> A. z e. B ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
79 75 78 sylibr 
 |-  ( ph -> ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) ) e. X_ z e. B ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
80 27 79 eqeltrd 
 |-  ( ph -> ( ( F N X ) ` A ) e. X_ z e. B ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
81 12 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> C e. Cat )
82 17 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> X e. B )
83 simpr1 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> z e. B )
84 1 2 81 82 40 83 yon11 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) = ( z ( Hom ` C ) X ) )
85 84 eleq2d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) <-> k e. ( z ( Hom ` C ) X ) ) )
86 85 biimpa 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ) -> k e. ( z ( Hom ` C ) X ) )
87 eqid 
 |-  ( comp ` O ) = ( comp ` O )
88 eqid 
 |-  ( comp ` S ) = ( comp ` S )
89 33 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
90 89 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( 1st ` F ) ( O Func S ) ( 2nd ` F ) )
91 82 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> X e. B )
92 83 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> z e. B )
93 simpr2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> w e. B )
94 93 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> w e. B )
95 simpr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> k e. ( z ( Hom ` C ) X ) )
96 95 41 eleqtrrdi 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> k e. ( X ( Hom ` O ) z ) )
97 simplr3 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> h e. ( z ( Hom ` O ) w ) )
98 28 29 87 88 90 91 92 94 96 97 funcco 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( X ( 2nd ` F ) w ) ` ( h ( <. X , z >. ( comp ` O ) w ) k ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` z ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( X ( 2nd ` F ) z ) ` k ) ) )
99 eqid 
 |-  ( comp ` C ) = ( comp ` C )
100 2 99 4 91 92 94 oppcco 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( h ( <. X , z >. ( comp ` O ) w ) k ) = ( k ( <. w , z >. ( comp ` C ) X ) h ) )
101 100 fveq2d 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( X ( 2nd ` F ) w ) ` ( h ( <. X , z >. ( comp ` O ) w ) k ) ) = ( ( X ( 2nd ` F ) w ) ` ( k ( <. w , z >. ( comp ` C ) X ) h ) ) )
102 45 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> U e. _V )
103 102 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> U e. _V )
104 53 ad2antrr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( 1st ` F ) ` X ) e. U )
105 55 3ad2antr1 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( 1st ` F ) ` z ) e. U )
106 105 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( 1st ` F ) ` z ) e. U )
107 52 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( 1st ` F ) : B --> U )
108 107 93 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( 1st ` F ) ` w ) e. U )
109 108 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( 1st ` F ) ` w ) e. U )
110 28 29 30 89 82 83 funcf2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( X ( 2nd ` F ) z ) : ( X ( Hom ` O ) z ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
111 110 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( X ( 2nd ` F ) z ) : ( X ( Hom ` O ) z ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
112 111 96 ffvelrnd 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( X ( 2nd ` F ) z ) ` k ) e. ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) )
113 5 103 30 104 106 elsetchom 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( X ( 2nd ` F ) z ) ` k ) e. ( ( ( 1st ` F ) ` X ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) <-> ( ( X ( 2nd ` F ) z ) ` k ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` z ) ) )
114 112 113 mpbid 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( X ( 2nd ` F ) z ) ` k ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` z ) )
115 28 29 30 89 83 93 funcf2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( z ( 2nd ` F ) w ) : ( z ( Hom ` O ) w ) --> ( ( ( 1st ` F ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` w ) ) )
116 simpr3 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> h e. ( z ( Hom ` O ) w ) )
117 115 116 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( z ( 2nd ` F ) w ) ` h ) e. ( ( ( 1st ` F ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` w ) ) )
118 5 102 30 105 108 elsetchom 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( z ( 2nd ` F ) w ) ` h ) e. ( ( ( 1st ` F ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` w ) ) <-> ( ( z ( 2nd ` F ) w ) ` h ) : ( ( 1st ` F ) ` z ) --> ( ( 1st ` F ) ` w ) ) )
119 117 118 mpbid 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( z ( 2nd ` F ) w ) ` h ) : ( ( 1st ` F ) ` z ) --> ( ( 1st ` F ) ` w ) )
120 119 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( z ( 2nd ` F ) w ) ` h ) : ( ( 1st ` F ) ` z ) --> ( ( 1st ` F ) ` w ) )
121 5 103 88 104 106 109 114 120 setcco 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( z ( 2nd ` F ) w ) ` h ) ( <. ( ( 1st ` F ) ` X ) , ( ( 1st ` F ) ` z ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( X ( 2nd ` F ) z ) ` k ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( X ( 2nd ` F ) z ) ` k ) ) )
122 98 101 121 3eqtr3d 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( X ( 2nd ` F ) w ) ` ( k ( <. w , z >. ( comp ` C ) X ) h ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( X ( 2nd ` F ) z ) ` k ) ) )
123 122 fveq1d 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( X ( 2nd ` F ) w ) ` ( k ( <. w , z >. ( comp ` C ) X ) h ) ) ` A ) = ( ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( X ( 2nd ` F ) z ) ` k ) ) ` A ) )
124 19 ad2antrr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> A e. ( ( 1st ` F ) ` X ) )
125 fvco3 
 |-  ( ( ( ( X ( 2nd ` F ) z ) ` k ) : ( ( 1st ` F ) ` X ) --> ( ( 1st ` F ) ` z ) /\ A e. ( ( 1st ` F ) ` X ) ) -> ( ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( X ( 2nd ` F ) z ) ` k ) ) ` A ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( X ( 2nd ` F ) z ) ` k ) ` A ) ) )
126 114 124 125 syl2anc 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( X ( 2nd ` F ) z ) ` k ) ) ` A ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( X ( 2nd ` F ) z ) ` k ) ` A ) ) )
127 123 126 eqtrd 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( X ( 2nd ` F ) w ) ` ( k ( <. w , z >. ( comp ` C ) X ) h ) ) ` A ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( X ( 2nd ` F ) z ) ` k ) ` A ) ) )
128 81 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> C e. Cat )
129 40 4 oppchom 
 |-  ( z ( Hom ` O ) w ) = ( w ( Hom ` C ) z )
130 97 129 eleqtrdi 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> h e. ( w ( Hom ` C ) z ) )
131 1 2 128 91 40 92 99 94 130 95 yon12 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ` k ) = ( k ( <. w , z >. ( comp ` C ) X ) h ) )
132 131 fveq2d 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( ( F N X ) ` A ) ` w ) ` ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ` k ) ) = ( ( ( ( F N X ) ` A ) ` w ) ` ( k ( <. w , z >. ( comp ` C ) X ) h ) ) )
133 13 ad2antrr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> V e. W )
134 14 ad2antrr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ran ( Homf ` C ) C_ U )
135 15 ad2antrr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
136 16 ad2antrr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> F e. ( O Func S ) )
137 2 40 99 128 94 92 91 130 95 catcocl 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( k ( <. w , z >. ( comp ` C ) X ) h ) e. ( w ( Hom ` C ) X ) )
138 1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 94 137 yonedalem4b 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( ( F N X ) ` A ) ` w ) ` ( k ( <. w , z >. ( comp ` C ) X ) h ) ) = ( ( ( X ( 2nd ` F ) w ) ` ( k ( <. w , z >. ( comp ` C ) X ) h ) ) ` A ) )
139 132 138 eqtrd 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( ( F N X ) ` A ) ` w ) ` ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ` k ) ) = ( ( ( X ( 2nd ` F ) w ) ` ( k ( <. w , z >. ( comp ` C ) X ) h ) ) ` A ) )
140 1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 92 95 yonedalem4b 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( ( F N X ) ` A ) ` z ) ` k ) = ( ( ( X ( 2nd ` F ) z ) ` k ) ` A ) )
141 140 fveq2d 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( ( F N X ) ` A ) ` z ) ` k ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( X ( 2nd ` F ) z ) ` k ) ` A ) ) )
142 127 139 141 3eqtr4d 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( z ( Hom ` C ) X ) ) -> ( ( ( ( F N X ) ` A ) ` w ) ` ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ` k ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( ( F N X ) ` A ) ` z ) ` k ) ) )
143 86 142 syldan 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) /\ k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ) -> ( ( ( ( F N X ) ` A ) ` w ) ` ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ` k ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( ( F N X ) ` A ) ` z ) ` k ) ) )
144 143 mpteq2dva 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) |-> ( ( ( ( F N X ) ` A ) ` w ) ` ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ` k ) ) ) = ( k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) |-> ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( ( F N X ) ` A ) ` z ) ` k ) ) ) )
145 fveq2 
 |-  ( z = w -> ( ( ( F N X ) ` A ) ` z ) = ( ( ( F N X ) ` A ) ` w ) )
146 fveq2 
 |-  ( z = w -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) = ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) )
147 fveq2 
 |-  ( z = w -> ( ( 1st ` F ) ` z ) = ( ( 1st ` F ) ` w ) )
148 145 146 147 feq123d 
 |-  ( z = w -> ( ( ( ( F N X ) ` A ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) <-> ( ( ( F N X ) ` A ) ` w ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) --> ( ( 1st ` F ) ` w ) ) )
149 27 fveq1d 
 |-  ( ph -> ( ( ( F N X ) ` A ) ` z ) = ( ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) ) ` z ) )
150 ovex 
 |-  ( z ( Hom ` C ) X ) e. _V
151 150 mptex 
 |-  ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) e. _V
152 eqid 
 |-  ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) ) = ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) )
153 152 fvmpt2 
 |-  ( ( z e. B /\ ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) e. _V ) -> ( ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) ) ` z ) = ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) )
154 151 153 mpan2 
 |-  ( z e. B -> ( ( z e. B |-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) ) ` z ) = ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) )
155 149 154 sylan9eq 
 |-  ( ( ph /\ z e. B ) -> ( ( ( F N X ) ` A ) ` z ) = ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) )
156 155 feq1d 
 |-  ( ( ph /\ z e. B ) -> ( ( ( ( F N X ) ` A ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) <-> ( g e. ( z ( Hom ` C ) X ) |-> ( ( ( X ( 2nd ` F ) z ) ` g ) ` A ) ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) ) )
157 65 156 mpbird 
 |-  ( ( ph /\ z e. B ) -> ( ( ( F N X ) ` A ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) )
158 157 ralrimiva 
 |-  ( ph -> A. z e. B ( ( ( F N X ) ` A ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) )
159 158 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> A. z e. B ( ( ( F N X ) ` A ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) )
160 148 159 93 rspcdva 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( F N X ) ` A ) ` w ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) --> ( ( 1st ` F ) ` w ) )
161 68 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( 1st ` ( ( 1st ` Y ) ` X ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` X ) ) )
162 28 29 30 161 83 93 funcf2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) : ( z ( Hom ` O ) w ) --> ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) ) )
163 162 116 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) ) )
164 72 3ad2antr1 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) e. U )
165 71 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( 1st ` ( ( 1st ` Y ) ` X ) ) : B --> U )
166 165 93 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) e. U )
167 5 102 30 164 166 elsetchom 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) ) <-> ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) ) )
168 163 167 mpbid 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) )
169 fcompt 
 |-  ( ( ( ( ( F N X ) ` A ) ` w ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) --> ( ( 1st ` F ) ` w ) /\ ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) ) -> ( ( ( ( F N X ) ` A ) ` w ) o. ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ) = ( k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) |-> ( ( ( ( F N X ) ` A ) ` w ) ` ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ` k ) ) ) )
170 160 168 169 syl2anc 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( ( F N X ) ` A ) ` w ) o. ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ) = ( k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) |-> ( ( ( ( F N X ) ` A ) ` w ) ` ( ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ` k ) ) ) )
171 157 3ad2antr1 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( F N X ) ` A ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) )
172 fcompt 
 |-  ( ( ( ( z ( 2nd ` F ) w ) ` h ) : ( ( 1st ` F ) ` z ) --> ( ( 1st ` F ) ` w ) /\ ( ( ( F N X ) ` A ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) --> ( ( 1st ` F ) ` z ) ) -> ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( ( F N X ) ` A ) ` z ) ) = ( k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) |-> ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( ( F N X ) ` A ) ` z ) ` k ) ) ) )
173 119 171 172 syl2anc 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( ( F N X ) ` A ) ` z ) ) = ( k e. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) |-> ( ( ( z ( 2nd ` F ) w ) ` h ) ` ( ( ( ( F N X ) ` A ) ` z ) ` k ) ) ) )
174 144 170 173 3eqtr4d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( ( F N X ) ` A ) ` w ) o. ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( ( F N X ) ` A ) ` z ) ) )
175 5 102 88 164 166 108 168 160 setcco 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( ( F N X ) ` A ) ` w ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ) = ( ( ( ( F N X ) ` A ) ` w ) o. ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ) )
176 5 102 88 164 105 108 171 119 setcco 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( z ( 2nd ` F ) w ) ` h ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) , ( ( 1st ` F ) ` z ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( ( F N X ) ` A ) ` z ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) o. ( ( ( F N X ) ` A ) ` z ) ) )
177 174 175 176 3eqtr4d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ h e. ( z ( Hom ` O ) w ) ) ) -> ( ( ( ( F N X ) ` A ) ` w ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) , ( ( 1st ` F ) ` z ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( ( F N X ) ` A ) ` z ) ) )
178 177 ralrimivvva 
 |-  ( ph -> A. z e. B A. w e. B A. h e. ( z ( Hom ` O ) w ) ( ( ( ( F N X ) ` A ) ` w ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) , ( ( 1st ` F ) ` z ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( ( F N X ) ` A ) ` z ) ) )
179 eqid 
 |-  ( O Nat S ) = ( O Nat S )
180 179 28 29 30 88 66 16 isnat2 
 |-  ( ph -> ( ( ( F N X ) ` A ) e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) <-> ( ( ( F N X ) ` A ) e. X_ z e. B ( ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) ( Hom ` S ) ( ( 1st ` F ) ` z ) ) /\ A. z e. B A. w e. B A. h e. ( z ( Hom ` O ) w ) ( ( ( ( F N X ) ` A ) ` w ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` w ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( z ( 2nd ` ( ( 1st ` Y ) ` X ) ) w ) ` h ) ) = ( ( ( z ( 2nd ` F ) w ) ` h ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` X ) ) ` z ) , ( ( 1st ` F ) ` z ) >. ( comp ` S ) ( ( 1st ` F ) ` w ) ) ( ( ( F N X ) ` A ) ` z ) ) ) ) )
181 80 178 180 mpbir2and 
 |-  ( ph -> ( ( F N X ) ` A ) e. ( ( ( 1st ` Y ) ` X ) ( O Nat S ) F ) )