Theorem yonedainv 16921

Description: The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)

Hypotheses

Ref	Expression
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 X.c 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 ) ) ⟨,⟩F ( Q 1stF O ) ) )
yoneda.c	|- ( ph -> C e. Cat )
yoneda.w	|- ( ph -> V e. W )
yoneda.u	|- ( ph -> ran ( Hom f ` C ) C_ U )
yoneda.v	|- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )
yoneda.m	|- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
yonedainv.i	|- I = (Inv ` R )
yonedainv.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 ) ) ) ) )

Assertion

Ref	Expression
yonedainv	|- ( ph -> M ( Z I E ) N )

Distinct variable groups:   f, a, g, x, y, .1.   u, a, g, y, C, f, x   E, a, f, g, u, y   B, a, f, g, u, x, y   N, a   O, a, f, g, u, x, y   S, a, f, g, u, x, y   g, M, u, y   Q, a, f, g, u, x   T, f, g, u, y   ph, a, f, g, u, x, y   u, R   Y, a, f, g, u, x, y   Z, a, f, g, u, x, y

Allowed substitution hints:   Q( y)   R( x, y, f, g, a)   T( x, a)   U( x, y, u, f, g, a)   .1. ( u)   E( x)   H( x, y, u, f, g, a)   I( x, y, u, f, g, a)   M( x, f, a)   N( x, y, u, f, g)   V( x, y, u, f, g, a)   W( x, y, u, f, g, a)

Proof of Theorem yonedainv

Dummy variables b h k w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		yoneda.r	. . 3 |- R = ( ( Q X.c O ) FuncCat T )
2		eqid 2622	. . . 4 |- ( Q X.c O ) = ( Q X.c O )
3		yoneda.q	. . . . 5 |- Q = ( O FuncCat S )
4	3	fucbas 16620	. . . 4 |- ( O Func S ) = ( Base ` Q )
5		yoneda.o	. . . . 5 |- O = (oppCat ` C )
6		yoneda.b	. . . . 5 |- B = ( Base ` C )
7	5, 6	oppcbas 16378	. . . 4 |- B = ( Base ` O )
8	2, 4, 7	xpcbas 16818	. . 3 |- ( ( O Func S ) X. B ) = ( Base ` ( Q X.c O ) )
9		eqid 2622	. . 3 |- ( ( Q X.c O ) Nat T ) = ( ( Q X.c O ) Nat T )
10		yoneda.y	. . . . 5 |- Y = (Yon ` C )
11		yoneda.1	. . . . 5 |- .1. = ( Id ` C )
12		yoneda.s	. . . . 5 |- S = ( SetCat ` U )
13		yoneda.t	. . . . 5 |- T = ( SetCat ` V )
14		yoneda.h	. . . . 5 |- H = (HomF ` Q )
15		yoneda.e	. . . . 5 |- E = ( O evalF S )
16		yoneda.z	. . . . 5 |- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) ⟨,⟩F ( Q 1stF O ) ) )
17		yoneda.c	. . . . 5 |- ( ph -> C e. Cat )
18		yoneda.w	. . . . 5 |- ( ph -> V e. W )
19		yoneda.u	. . . . 5 |- ( ph -> ran ( Hom f ` C ) C_ U )
20		yoneda.v	. . . . 5 |- ( ph -> ( ran ( Hom f ` Q ) u. U ) C_ V )
21	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20	yonedalem1 16912	. . . 4 |- ( ph -> ( Z e. ( ( Q X.c O ) Func T ) /\ E e. ( ( Q X.c O ) Func T ) ) )
22	21	simpld 475	. . 3 |- ( ph -> Z e. ( ( Q X.c O ) Func T ) )
23	21	simprd 479	. . 3 |- ( ph -> E e. ( ( Q X.c O ) Func T ) )
24		yonedainv.i	. . 3 |- I = (Inv ` R )
25		eqid 2622	. . 3 |- (Inv ` T ) = (Inv ` T )
26		yoneda.m	. . . 4 |- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
27	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26	yonedalem3 16920	. . 3 |- ( ph -> M e. ( Z ( ( Q X.c O ) Nat T ) E ) )
28	17	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> C e. Cat )
29	18	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> V e. W )
30	19	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ran ( Hom f ` C ) C_ U )
31	20	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ran ( Hom f ` Q ) u. U ) C_ V )
32		simprl 794	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> h e. ( O Func S ) )
33		simprr 796	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> w e. B )
34	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26	yonedalem3a 16914	. . . . . . . . . 10 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) = ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) /\ ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) ) )
35	34	simprd 479	. . . . . . . . 9 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) )
36	28	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> C e. Cat )
37	29	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> V e. W )
38	30	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> ran ( Hom f ` C ) C_ U )
39	31	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> ( ran ( Hom f ` Q ) u. U ) C_ V )
40		simplrl 800	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> h e. ( O Func S ) )
41		simplrr 801	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> w e. B )
42		yonedainv.n	. . . . . . . . . . . 12 |- 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 ) ) ) ) )
43		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> b e. ( ( 1st ` h ) ` w ) )
44	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43	yonedalem4c 16917	. . . . . . . . . . 11 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> ( ( h N w ) ` b ) e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
45		eqid 2622	. . . . . . . . . . 11 |- ( b e. ( ( 1st ` h ) ` w ) |-> ( ( h N w ) ` b ) ) = ( b e. ( ( 1st ` h ) ` w ) |-> ( ( h N w ) ` b ) )
46	44, 45	fmptd 6385	. . . . . . . . . 10 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( b e. ( ( 1st ` h ) ` w ) |-> ( ( h N w ) ` b ) ) : ( ( 1st ` h ) ` w ) --> ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
47		fvex 6201	. . . . . . . . . . . . . . . 16 |- ( Base ` C ) e. _V
48	6, 47	eqeltri 2697	. . . . . . . . . . . . . . 15 |- B e. _V
49	48	mptex 6486	. . . . . . . . . . . . . 14 |- ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) e. _V
50		eqid 2622	. . . . . . . . . . . . . 14 |- ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) = ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) )
51	49, 50	fnmpti 6022	. . . . . . . . . . . . 13 |- ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) Fn ( ( 1st ` h ) ` w )
52		simpl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( f = h /\ x = w ) -> f = h )
53	52	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( f = h /\ x = w ) -> ( 1st ` f ) = ( 1st ` h ) )
54		simpr 477	. . . . . . . . . . . . . . . . . 18 |- ( ( f = h /\ x = w ) -> x = w )
55	53, 54	fveq12d 6197	. . . . . . . . . . . . . . . . 17 |- ( ( f = h /\ x = w ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` h ) ` w ) )
56		simplr 792	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> x = w )
57	56	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( y ( Hom ` C ) x ) = ( y ( Hom ` C ) w ) )
58		simpll 790	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> f = h )
59	58	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( 2nd ` f ) = ( 2nd ` h ) )
60		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> y = y )
61	59, 56, 60	oveq123d 6671	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( x ( 2nd ` f ) y ) = ( w ( 2nd ` h ) y ) )
62	61	fveq1d 6193	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( ( x ( 2nd ` f ) y ) ` g ) = ( ( w ( 2nd ` h ) y ) ` g ) )
63	62	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) = ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) )
64	57, 63	mpteq12dv 4733	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f = h /\ x = w ) /\ y e. B ) -> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) = ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) )
65	64	mpteq2dva 4744	. . . . . . . . . . . . . . . . 17 |- ( ( f = h /\ x = w ) -> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) = ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) )
66	55, 65	mpteq12dv 4733	. . . . . . . . . . . . . . . 16 |- ( ( f = h /\ x = w ) -> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) = ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) )
67		fvex 6201	. . . . . . . . . . . . . . . . 17 |- ( ( 1st ` h ) ` w ) e. _V
68	67	mptex 6486	. . . . . . . . . . . . . . . 16 |- ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) e. _V
69	66, 42, 68	ovmpt2a 6791	. . . . . . . . . . . . . . 15 |- ( ( h e. ( O Func S ) /\ w e. B ) -> ( h N w ) = ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) )
70	69	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) = ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) )
71	70	fneq1d 5981	. . . . . . . . . . . . 13 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h N w ) Fn ( ( 1st ` h ) ` w ) <-> ( u e. ( ( 1st ` h ) ` w ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) w ) |-> ( ( ( w ( 2nd ` h ) y ) ` g ) ` u ) ) ) ) Fn ( ( 1st ` h ) ` w ) ) )
72	51, 71	mpbiri 248	. . . . . . . . . . . 12 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) Fn ( ( 1st ` h ) ` w ) )
73		dffn5 6241	. . . . . . . . . . . 12 |- ( ( h N w ) Fn ( ( 1st ` h ) ` w ) <-> ( h N w ) = ( b e. ( ( 1st ` h ) ` w ) |-> ( ( h N w ) ` b ) ) )
74	72, 73	sylib 208	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) = ( b e. ( ( 1st ` h ) ` w ) |-> ( ( h N w ) ` b ) ) )
75	5	oppccat 16382	. . . . . . . . . . . . . 14 |- ( C e. Cat -> O e. Cat )
76	17, 75	syl 17	. . . . . . . . . . . . 13 |- ( ph -> O e. Cat )
77	76	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> O e. Cat )
78	20	unssbd 3791	. . . . . . . . . . . . . . 15 |- ( ph -> U C_ V )
79	18, 78	ssexd 4805	. . . . . . . . . . . . . 14 |- ( ph -> U e. _V )
80	12	setccat 16735	. . . . . . . . . . . . . 14 |- ( U e. _V -> S e. Cat )
81	79, 80	syl 17	. . . . . . . . . . . . 13 |- ( ph -> S e. Cat )
82	81	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> S e. Cat )
83	15, 77, 82, 7, 32, 33	evlf1 16860	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h ( 1st ` E ) w ) = ( ( 1st ` h ) ` w ) )
84	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33	yonedalem21 16913	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h ( 1st ` Z ) w ) = ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
85	74, 83, 84	feq123d 6034	. . . . . . . . . 10 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h N w ) : ( h ( 1st ` E ) w ) --> ( h ( 1st ` Z ) w ) <-> ( b e. ( ( 1st ` h ) ` w ) |-> ( ( h N w ) ` b ) ) : ( ( 1st ` h ) ` w ) --> ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) ) )
86	46, 85	mpbird 247	. . . . . . . . 9 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) : ( h ( 1st ` E ) w ) --> ( h ( 1st ` Z ) w ) )
87		fcompt 6400	. . . . . . . . . . 11 |- ( ( ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) /\ ( h N w ) : ( h ( 1st ` E ) w ) --> ( h ( 1st ` Z ) w ) ) -> ( ( h M w ) o. ( h N w ) ) = ( k e. ( h ( 1st ` E ) w ) |-> ( ( h M w ) ` ( ( h N w ) ` k ) ) ) )
88	35, 86, 87	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) o. ( h N w ) ) = ( k e. ( h ( 1st ` E ) w ) |-> ( ( h M w ) ` ( ( h N w ) ` k ) ) ) )
89	83	eleq2d 2687	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( k e. ( h ( 1st ` E ) w ) <-> k e. ( ( 1st ` h ) ` w ) ) )
90	89	biimpa 501	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( h ( 1st ` E ) w ) ) -> k e. ( ( 1st ` h ) ` w ) )
91	28	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> C e. Cat )
92	29	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> V e. W )
93	30	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ran ( Hom f ` C ) C_ U )
94	31	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ran ( Hom f ` Q ) u. U ) C_ V )
95		simplrl 800	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> h e. ( O Func S ) )
96		simplrr 801	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> w e. B )
97	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 26	yonedalem3a 16914	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( h M w ) = ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) /\ ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) ) )
98	97	simpld 475	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( h M w ) = ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) )
99	98	fveq1d 6193	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( h M w ) ` ( ( h N w ) ` k ) ) = ( ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) ` ( ( h N w ) ` k ) ) )
100		fvexd 6203	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( ( 1st ` h ) ` w ) ) -> ( ( h N w ) ` b ) e. _V )
101	100, 74, 44	fmpt2d 6393	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h N w ) : ( ( 1st ` h ) ` w ) --> ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
102	101	ffvelrnda 6359	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( h N w ) ` k ) e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
103		fveq1 6190	. . . . . . . . . . . . . . . . 17 |- ( a = ( ( h N w ) ` k ) -> ( a ` w ) = ( ( ( h N w ) ` k ) ` w ) )
104	103	fveq1d 6193	. . . . . . . . . . . . . . . 16 |- ( a = ( ( h N w ) ` k ) -> ( ( a ` w ) ` ( .1. ` w ) ) = ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) )
105		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) = ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) )
106		fvex 6201	. . . . . . . . . . . . . . . 16 |- ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) e. _V
107	104, 105, 106	fvmpt 6282	. . . . . . . . . . . . . . 15 |- ( ( ( h N w ) ` k ) e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) -> ( ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) ` ( ( h N w ) ` k ) ) = ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) )
108	102, 107	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) ` ( ( h N w ) ` k ) ) = ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) )
109		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> k e. ( ( 1st ` h ) ` w ) )
110		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( Hom ` C ) = ( Hom ` C )
111	6, 110, 11, 91, 96	catidcl 16343	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( .1. ` w ) e. ( w ( Hom ` C ) w ) )
112	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 42, 109, 96, 111	yonedalem4b 16916	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) = ( ( ( w ( 2nd ` h ) w ) ` ( .1. ` w ) ) ` k ) )
113		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( Id ` O ) = ( Id ` O )
114		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( Id ` S ) = ( Id ` S )
115		relfunc 16522	. . . . . . . . . . . . . . . . . . 19 |- Rel ( O Func S )
116		1st2ndbr 7217	. . . . . . . . . . . . . . . . . . 19 |- ( ( Rel ( O Func S ) /\ h e. ( O Func S ) ) -> ( 1st ` h ) ( O Func S ) ( 2nd ` h ) )
117	115, 95, 116	sylancr 695	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( 1st ` h ) ( O Func S ) ( 2nd ` h ) )
118	7, 113, 114, 117, 96	funcid 16530	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( w ( 2nd ` h ) w ) ` ( ( Id ` O ) ` w ) ) = ( ( Id ` S ) ` ( ( 1st ` h ) ` w ) ) )
119	5, 11	oppcid 16381	. . . . . . . . . . . . . . . . . . . 20 |- ( C e. Cat -> ( Id ` O ) = .1. )
120	91, 119	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( Id ` O ) = .1. )
121	120	fveq1d 6193	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( Id ` O ) ` w ) = ( .1. ` w ) )
122	121	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( w ( 2nd ` h ) w ) ` ( ( Id ` O ) ` w ) ) = ( ( w ( 2nd ` h ) w ) ` ( .1. ` w ) ) )
123	79	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> U e. _V )
124		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 |- ( Base ` S ) = ( Base ` S )
125	7, 124, 117	funcf1 16526	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( 1st ` h ) : B --> ( Base ` S ) )
126	12, 123	setcbas 16728	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> U = ( Base ` S ) )
127	126	feq3d 6032	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( 1st ` h ) : B --> U <-> ( 1st ` h ) : B --> ( Base ` S ) ) )
128	125, 127	mpbird 247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( 1st ` h ) : B --> U )
129	128, 96	ffvelrnd 6360	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( 1st ` h ) ` w ) e. U )
130	12, 114, 123, 129	setcid 16736	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( Id ` S ) ` ( ( 1st ` h ) ` w ) ) = ( _I |` ( ( 1st ` h ) ` w ) ) )
131	118, 122, 130	3eqtr3d 2664	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( w ( 2nd ` h ) w ) ` ( .1. ` w ) ) = ( _I |` ( ( 1st ` h ) ` w ) ) )
132	131	fveq1d 6193	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( ( w ( 2nd ` h ) w ) ` ( .1. ` w ) ) ` k ) = ( ( _I |` ( ( 1st ` h ) ` w ) ) ` k ) )
133		fvresi 6439	. . . . . . . . . . . . . . . 16 |- ( k e. ( ( 1st ` h ) ` w ) -> ( ( _I |` ( ( 1st ` h ) ` w ) ) ` k ) = k )
134	133	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( _I |` ( ( 1st ` h ) ` w ) ) ` k ) = k )
135	112, 132, 134	3eqtrd 2660	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( ( ( h N w ) ` k ) ` w ) ` ( .1. ` w ) ) = k )
136	99, 108, 135	3eqtrd 2660	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( ( 1st ` h ) ` w ) ) -> ( ( h M w ) ` ( ( h N w ) ` k ) ) = k )
137	90, 136	syldan 487	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ k e. ( h ( 1st ` E ) w ) ) -> ( ( h M w ) ` ( ( h N w ) ` k ) ) = k )
138	137	mpteq2dva 4744	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( k e. ( h ( 1st ` E ) w ) |-> ( ( h M w ) ` ( ( h N w ) ` k ) ) ) = ( k e. ( h ( 1st ` E ) w ) |-> k ) )
139		mptresid 5456	. . . . . . . . . . 11 |- ( k e. ( h ( 1st ` E ) w ) |-> k ) = ( _I |` ( h ( 1st ` E ) w ) )
140	138, 139	syl6eq 2672	. . . . . . . . . 10 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( k e. ( h ( 1st ` E ) w ) |-> ( ( h M w ) ` ( ( h N w ) ` k ) ) ) = ( _I |` ( h ( 1st ` E ) w ) ) )
141	88, 140	eqtrd 2656	. . . . . . . . 9 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) o. ( h N w ) ) = ( _I |` ( h ( 1st ` E ) w ) ) )
142		fcompt 6400	. . . . . . . . . . 11 |- ( ( ( h N w ) : ( h ( 1st ` E ) w ) --> ( h ( 1st ` Z ) w ) /\ ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) ) -> ( ( h N w ) o. ( h M w ) ) = ( b e. ( h ( 1st ` Z ) w ) |-> ( ( h N w ) ` ( ( h M w ) ` b ) ) ) )
143	86, 35, 142	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h N w ) o. ( h M w ) ) = ( b e. ( h ( 1st ` Z ) w ) |-> ( ( h N w ) ` ( ( h M w ) ` b ) ) ) )
144		eqid 2622	. . . . . . . . . . . . . 14 |- ( O Nat S ) = ( O Nat S )
145	28	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> C e. Cat )
146	29	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> V e. W )
147	30	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ran ( Hom f ` C ) C_ U )
148	31	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ran ( Hom f ` Q ) u. U ) C_ V )
149		simplrl 800	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> h e. ( O Func S ) )
150		simplrr 801	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> w e. B )
151	83	feq3d 6032	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) <-> ( h M w ) : ( h ( 1st ` Z ) w ) --> ( ( 1st ` h ) ` w ) ) )
152	35, 151	mpbid 222	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h M w ) : ( h ( 1st ` Z ) w ) --> ( ( 1st ` h ) ` w ) )
153	152	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( h M w ) ` b ) e. ( ( 1st ` h ) ` w ) )
154	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 145, 146, 147, 148, 149, 150, 42, 153	yonedalem4c 16917	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( h N w ) ` ( ( h M w ) ` b ) ) e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
155	144, 154	nat1st2nd 16611	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( h N w ) ` ( ( h M w ) ` b ) ) e. ( <. ( 1st ` ( ( 1st ` Y ) ` w ) ) , ( 2nd ` ( ( 1st ` Y ) ` w ) ) >. ( O Nat S ) <. ( 1st ` h ) , ( 2nd ` h ) >. ) )
156	144, 155, 7	natfn 16614	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( h N w ) ` ( ( h M w ) ` b ) ) Fn B )
157	84	eleq2d 2687	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( b e. ( h ( 1st ` Z ) w ) <-> b e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) ) )
158	157	biimpa 501	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> b e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
159	144, 158	nat1st2nd 16611	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> b e. ( <. ( 1st ` ( ( 1st ` Y ) ` w ) ) , ( 2nd ` ( ( 1st ` Y ) ` w ) ) >. ( O Nat S ) <. ( 1st ` h ) , ( 2nd ` h ) >. ) )
160	144, 159, 7	natfn 16614	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> b Fn B )
161	145	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> C e. Cat )
162	150	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> w e. B )
163		simpr 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> z e. B )
164	10, 6, 161, 162, 110, 163	yon11 16904	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) = ( z ( Hom ` C ) w ) )
165	164	eleq2d 2687	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( k e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) <-> k e. ( z ( Hom ` C ) w ) ) )
166	165	biimpa 501	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ) -> k e. ( z ( Hom ` C ) w ) )
167	161	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> C e. Cat )
168	146	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> V e. W )
169	147	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ran ( Hom f ` C ) C_ U )
170	148	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ran ( Hom f ` Q ) u. U ) C_ V )
171	149	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> h e. ( O Func S ) )
172	162	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> w e. B )
173	153	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( h M w ) ` b ) e. ( ( 1st ` h ) ` w ) )
174		simplr 792	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> z e. B )
175		simpr 477	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> k e. ( z ( Hom ` C ) w ) )
176	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 167, 168, 169, 170, 171, 172, 42, 173, 174, 175	yonedalem4b 16916	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) ` k ) = ( ( ( w ( 2nd ` h ) z ) ` k ) ` ( ( h M w ) ` b ) ) )
177	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 167, 168, 169, 170, 171, 172, 26	yonedalem3a 16914	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( h M w ) = ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) /\ ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) ) )
178	177	simpld 475	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( h M w ) = ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) )
179	178	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( h M w ) ` b ) = ( ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) ` b ) )
180	158	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> b e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) )
181		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = b -> ( a ` w ) = ( b ` w ) )
182	181	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = b -> ( ( a ` w ) ` ( .1. ` w ) ) = ( ( b ` w ) ` ( .1. ` w ) ) )
183		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( b ` w ) ` ( .1. ` w ) ) e. _V
184	182, 105, 183	fvmpt 6282	. . . . . . . . . . . . . . . . . . . 20 |- ( b e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) -> ( ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) ` b ) = ( ( b ` w ) ` ( .1. ` w ) ) )
185	180, 184	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( a e. ( ( ( 1st ` Y ) ` w ) ( O Nat S ) h ) |-> ( ( a ` w ) ` ( .1. ` w ) ) ) ` b ) = ( ( b ` w ) ` ( .1. ` w ) ) )
186	179, 185	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( h M w ) ` b ) = ( ( b ` w ) ` ( .1. ` w ) ) )
187	186	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( w ( 2nd ` h ) z ) ` k ) ` ( ( h M w ) ` b ) ) = ( ( ( w ( 2nd ` h ) z ) ` k ) ` ( ( b ` w ) ` ( .1. ` w ) ) ) )
188	159	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> b e. ( <. ( 1st ` ( ( 1st ` Y ) ` w ) ) , ( 2nd ` ( ( 1st ` Y ) ` w ) ) >. ( O Nat S ) <. ( 1st ` h ) , ( 2nd ` h ) >. ) )
189		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Hom ` O ) = ( Hom ` O )
190		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 |- (comp ` S ) = (comp ` S )
191	110, 5	oppchom 16375	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w ( Hom ` O ) z ) = ( z ( Hom ` C ) w )
192	175, 191	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> k e. ( w ( Hom ` O ) z ) )
193	144, 188, 7, 189, 190, 172, 174, 192	nati 16615	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( b ` z ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) , ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) >. (comp ` S ) ( ( 1st ` h ) ` z ) ) ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ) = ( ( ( w ( 2nd ` h ) z ) ` k ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) , ( ( 1st ` h ) ` w ) >. (comp ` S ) ( ( 1st ` h ) ` z ) ) ( b ` w ) ) )
194	79	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> U e. _V )
195	194	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> U e. _V )
196	195	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> U e. _V )
197		relfunc 16522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- Rel ( C Func Q )
198	10, 17, 5, 12, 3, 79, 19	yoncl 16902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> Y e. ( C Func Q ) )
199		1st2ndbr 7217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( Rel ( C Func Q ) /\ Y e. ( C Func Q ) ) -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
200	197, 198, 199	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
201	6, 4, 200	funcf1 16526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> ( 1st ` Y ) : B --> ( O Func S ) )
202	201	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` Y ) : B --> ( O Func S ) )
203	202, 150	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` Y ) ` w ) e. ( O Func S ) )
204		1st2ndbr 7217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( Rel ( O Func S ) /\ ( ( 1st ` Y ) ` w ) e. ( O Func S ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` w ) ) )
205	115, 203, 204	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` w ) ) )
206	7, 124, 205	funcf1 16526	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) : B --> ( Base ` S ) )
207	12, 194	setcbas 16728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> U = ( Base ` S ) )
208	207	feq3d 6032	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) : B --> U <-> ( 1st ` ( ( 1st ` Y ) ` w ) ) : B --> ( Base ` S ) ) )
209	206, 208	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) : B --> U )
210	209, 150	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) e. U )
211	210	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) e. U )
212	209	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) e. U )
213	212	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) e. U )
214	115, 149, 116	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` h ) ( O Func S ) ( 2nd ` h ) )
215	7, 124, 214	funcf1 16526	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` h ) : B --> ( Base ` S ) )
216	207	feq3d 6032	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` h ) : B --> U <-> ( 1st ` h ) : B --> ( Base ` S ) ) )
217	215, 216	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( 1st ` h ) : B --> U )
218	217	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( 1st ` h ) ` z ) e. U )
219	218	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( 1st ` h ) ` z ) e. U )
220		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( Hom ` S ) = ( Hom ` S )
221	205	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` w ) ) )
222	7, 189, 220, 221, 172, 174	funcf2 16528	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) : ( w ( Hom ` O ) z ) --> ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ) )
223	222, 192	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ) )
224	12, 196, 220, 211, 213	elsetchom 16731	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) ( Hom ` S ) ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ) <-> ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) --> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ) )
225	223, 224	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) --> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) )
226	159	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> b e. ( <. ( 1st ` ( ( 1st ` Y ) ` w ) ) , ( 2nd ` ( ( 1st ` Y ) ` w ) ) >. ( O Nat S ) <. ( 1st ` h ) , ( 2nd ` h ) >. ) )
227	144, 226, 7, 220, 163	natcl 16613	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( b ` z ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ( Hom ` S ) ( ( 1st ` h ) ` z ) ) )
228	12, 195, 220, 212, 218	elsetchom 16731	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( b ` z ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ( Hom ` S ) ( ( 1st ` h ) ` z ) ) <-> ( b ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) --> ( ( 1st ` h ) ` z ) ) )
229	227, 228	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( b ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) --> ( ( 1st ` h ) ` z ) )
230	229	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( b ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) --> ( ( 1st ` h ) ` z ) )
231	12, 196, 190, 211, 213, 219, 225, 230	setcco 16733	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( b ` z ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) , ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) >. (comp ` S ) ( ( 1st ` h ) ` z ) ) ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ) = ( ( b ` z ) o. ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ) )
232	217, 150	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` h ) ` w ) e. U )
233	232	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( 1st ` h ) ` w ) e. U )
234	144, 159, 7, 220, 150	natcl 16613	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( b ` w ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) ( Hom ` S ) ( ( 1st ` h ) ` w ) ) )
235	12, 194, 220, 210, 232	elsetchom 16731	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( b ` w ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) ( Hom ` S ) ( ( 1st ` h ) ` w ) ) <-> ( b ` w ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) --> ( ( 1st ` h ) ` w ) ) )
236	234, 235	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( b ` w ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) --> ( ( 1st ` h ) ` w ) )
237	236	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( b ` w ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) --> ( ( 1st ` h ) ` w ) )
238	115, 171, 116	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( 1st ` h ) ( O Func S ) ( 2nd ` h ) )
239	7, 189, 220, 238, 172, 174	funcf2 16528	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( w ( 2nd ` h ) z ) : ( w ( Hom ` O ) z ) --> ( ( ( 1st ` h ) ` w ) ( Hom ` S ) ( ( 1st ` h ) ` z ) ) )
240	239, 192	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( w ( 2nd ` h ) z ) ` k ) e. ( ( ( 1st ` h ) ` w ) ( Hom ` S ) ( ( 1st ` h ) ` z ) ) )
241	12, 196, 220, 233, 219	elsetchom 16731	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( w ( 2nd ` h ) z ) ` k ) e. ( ( ( 1st ` h ) ` w ) ( Hom ` S ) ( ( 1st ` h ) ` z ) ) <-> ( ( w ( 2nd ` h ) z ) ` k ) : ( ( 1st ` h ) ` w ) --> ( ( 1st ` h ) ` z ) ) )
242	240, 241	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( w ( 2nd ` h ) z ) ` k ) : ( ( 1st ` h ) ` w ) --> ( ( 1st ` h ) ` z ) )
243	12, 196, 190, 211, 233, 219, 237, 242	setcco 16733	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( w ( 2nd ` h ) z ) ` k ) ( <. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) , ( ( 1st ` h ) ` w ) >. (comp ` S ) ( ( 1st ` h ) ` z ) ) ( b ` w ) ) = ( ( ( w ( 2nd ` h ) z ) ` k ) o. ( b ` w ) ) )
244	193, 231, 243	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( b ` z ) o. ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ) = ( ( ( w ( 2nd ` h ) z ) ` k ) o. ( b ` w ) ) )
245	244	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( b ` z ) o. ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ) ` ( .1. ` w ) ) = ( ( ( ( w ( 2nd ` h ) z ) ` k ) o. ( b ` w ) ) ` ( .1. ` w ) ) )
246	6, 110, 11, 145, 150	catidcl 16343	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( .1. ` w ) e. ( w ( Hom ` C ) w ) )
247	10, 6, 145, 150, 110, 150	yon11 16904	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) = ( w ( Hom ` C ) w ) )
248	246, 247	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( .1. ` w ) e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) )
249	248	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( .1. ` w ) e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) )
250		fvco3 6275	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) --> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) /\ ( .1. ` w ) e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) ) -> ( ( ( b ` z ) o. ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ) ` ( .1. ` w ) ) = ( ( b ` z ) ` ( ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ` ( .1. ` w ) ) ) )
251	225, 249, 250	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( b ` z ) o. ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ) ` ( .1. ` w ) ) = ( ( b ` z ) ` ( ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ` ( .1. ` w ) ) ) )
252		fvco3 6275	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( b ` w ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) --> ( ( 1st ` h ) ` w ) /\ ( .1. ` w ) e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` w ) ) -> ( ( ( ( w ( 2nd ` h ) z ) ` k ) o. ( b ` w ) ) ` ( .1. ` w ) ) = ( ( ( w ( 2nd ` h ) z ) ` k ) ` ( ( b ` w ) ` ( .1. ` w ) ) ) )
253	236, 248, 252	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( ( ( w ( 2nd ` h ) z ) ` k ) o. ( b ` w ) ) ` ( .1. ` w ) ) = ( ( ( w ( 2nd ` h ) z ) ` k ) ` ( ( b ` w ) ` ( .1. ` w ) ) ) )
254	253	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( ( w ( 2nd ` h ) z ) ` k ) o. ( b ` w ) ) ` ( .1. ` w ) ) = ( ( ( w ( 2nd ` h ) z ) ` k ) ` ( ( b ` w ) ` ( .1. ` w ) ) ) )
255	245, 251, 254	3eqtr3d 2664	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( b ` z ) ` ( ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ` ( .1. ` w ) ) ) = ( ( ( w ( 2nd ` h ) z ) ` k ) ` ( ( b ` w ) ` ( .1. ` w ) ) ) )
256		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 |- (comp ` C ) = (comp ` C )
257	246	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( .1. ` w ) e. ( w ( Hom ` C ) w ) )
258	10, 6, 167, 172, 110, 172, 256, 174, 175, 257	yon12 16905	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ` ( .1. ` w ) ) = ( ( .1. ` w ) ( <. z , w >. (comp ` C ) w ) k ) )
259	6, 110, 11, 167, 174, 256, 172, 175	catlid 16344	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( .1. ` w ) ( <. z , w >. (comp ` C ) w ) k ) = k )
260	258, 259	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ` ( .1. ` w ) ) = k )
261	260	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( b ` z ) ` ( ( ( w ( 2nd ` ( ( 1st ` Y ) ` w ) ) z ) ` k ) ` ( .1. ` w ) ) ) = ( ( b ` z ) ` k ) )
262	255, 261	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( w ( 2nd ` h ) z ) ` k ) ` ( ( b ` w ) ` ( .1. ` w ) ) ) = ( ( b ` z ) ` k ) )
263	176, 187, 262	3eqtrd 2660	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( z ( Hom ` C ) w ) ) -> ( ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) ` k ) = ( ( b ` z ) ` k ) )
264	166, 263	syldan 487	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) /\ k e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ) -> ( ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) ` k ) = ( ( b ` z ) ` k ) )
265	264	mpteq2dva 4744	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( k e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) |-> ( ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) ` k ) ) = ( k e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) |-> ( ( b ` z ) ` k ) ) )
266	155	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( h N w ) ` ( ( h M w ) ` b ) ) e. ( <. ( 1st ` ( ( 1st ` Y ) ` w ) ) , ( 2nd ` ( ( 1st ` Y ) ` w ) ) >. ( O Nat S ) <. ( 1st ` h ) , ( 2nd ` h ) >. ) )
267	144, 266, 7, 220, 163	natcl 16613	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ( Hom ` S ) ( ( 1st ` h ) ` z ) ) )
268	12, 195, 220, 212, 218	elsetchom 16731	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) e. ( ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) ( Hom ` S ) ( ( 1st ` h ) ` z ) ) <-> ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) --> ( ( 1st ` h ) ` z ) ) )
269	267, 268	mpbid 222	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) : ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) --> ( ( 1st ` h ) ` z ) )
270	269	feqmptd 6249	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) = ( k e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) |-> ( ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) ` k ) ) )
271	229	feqmptd 6249	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( b ` z ) = ( k e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) |-> ( ( b ` z ) ` k ) ) )
272	265, 270, 271	3eqtr4d 2666	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) /\ z e. B ) -> ( ( ( h N w ) ` ( ( h M w ) ` b ) ) ` z ) = ( b ` z ) )
273	156, 160, 272	eqfnfvd 6314	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) /\ b e. ( h ( 1st ` Z ) w ) ) -> ( ( h N w ) ` ( ( h M w ) ` b ) ) = b )
274	273	mpteq2dva 4744	. . . . . . . . . . 11 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( b e. ( h ( 1st ` Z ) w ) |-> ( ( h N w ) ` ( ( h M w ) ` b ) ) ) = ( b e. ( h ( 1st ` Z ) w ) |-> b ) )
275		mptresid 5456	. . . . . . . . . . 11 |- ( b e. ( h ( 1st ` Z ) w ) |-> b ) = ( _I |` ( h ( 1st ` Z ) w ) )
276	274, 275	syl6eq 2672	. . . . . . . . . 10 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( b e. ( h ( 1st ` Z ) w ) |-> ( ( h N w ) ` ( ( h M w ) ` b ) ) ) = ( _I |` ( h ( 1st ` Z ) w ) ) )
277	143, 276	eqtrd 2656	. . . . . . . . 9 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h N w ) o. ( h M w ) ) = ( _I |` ( h ( 1st ` Z ) w ) ) )
278		fcof1o 6551	. . . . . . . . 9 |- ( ( ( ( h M w ) : ( h ( 1st ` Z ) w ) --> ( h ( 1st ` E ) w ) /\ ( h N w ) : ( h ( 1st ` E ) w ) --> ( h ( 1st ` Z ) w ) ) /\ ( ( ( h M w ) o. ( h N w ) ) = ( _I |` ( h ( 1st ` E ) w ) ) /\ ( ( h N w ) o. ( h M w ) ) = ( _I |` ( h ( 1st ` Z ) w ) ) ) ) -> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ `' ( h M w ) = ( h N w ) ) )
279	35, 86, 141, 277, 278	syl22anc 1327	. . . . . . . 8 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ `' ( h M w ) = ( h N w ) ) )
280		eqcom 2629	. . . . . . . . 9 |- ( `' ( h M w ) = ( h N w ) <-> ( h N w ) = `' ( h M w ) )
281	280	anbi2i 730	. . . . . . . 8 |- ( ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ `' ( h M w ) = ( h N w ) ) <-> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ ( h N w ) = `' ( h M w ) ) )
282	279, 281	sylib 208	. . . . . . 7 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ ( h N w ) = `' ( h M w ) ) )
283		eqid 2622	. . . . . . . . . . 11 |- ( Base ` T ) = ( Base ` T )
284		relfunc 16522	. . . . . . . . . . . 12 |- Rel ( ( Q X.c O ) Func T )
285		1st2ndbr 7217	. . . . . . . . . . . 12 |- ( ( Rel ( ( Q X.c O ) Func T ) /\ Z e. ( ( Q X.c O ) Func T ) ) -> ( 1st ` Z ) ( ( Q X.c O ) Func T ) ( 2nd ` Z ) )
286	284, 22, 285	sylancr 695	. . . . . . . . . . 11 |- ( ph -> ( 1st ` Z ) ( ( Q X.c O ) Func T ) ( 2nd ` Z ) )
287	8, 283, 286	funcf1 16526	. . . . . . . . . 10 |- ( ph -> ( 1st ` Z ) : ( ( O Func S ) X. B ) --> ( Base ` T ) )
288	13, 18	setcbas 16728	. . . . . . . . . . 11 |- ( ph -> V = ( Base ` T ) )
289	288	feq3d 6032	. . . . . . . . . 10 |- ( ph -> ( ( 1st ` Z ) : ( ( O Func S ) X. B ) --> V <-> ( 1st ` Z ) : ( ( O Func S ) X. B ) --> ( Base ` T ) ) )
290	287, 289	mpbird 247	. . . . . . . . 9 |- ( ph -> ( 1st ` Z ) : ( ( O Func S ) X. B ) --> V )
291	290	fovrnda 6805	. . . . . . . 8 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h ( 1st ` Z ) w ) e. V )
292		1st2ndbr 7217	. . . . . . . . . . . 12 |- ( ( Rel ( ( Q X.c O ) Func T ) /\ E e. ( ( Q X.c O ) Func T ) ) -> ( 1st ` E ) ( ( Q X.c O ) Func T ) ( 2nd ` E ) )
293	284, 23, 292	sylancr 695	. . . . . . . . . . 11 |- ( ph -> ( 1st ` E ) ( ( Q X.c O ) Func T ) ( 2nd ` E ) )
294	8, 283, 293	funcf1 16526	. . . . . . . . . 10 |- ( ph -> ( 1st ` E ) : ( ( O Func S ) X. B ) --> ( Base ` T ) )
295	288	feq3d 6032	. . . . . . . . . 10 |- ( ph -> ( ( 1st ` E ) : ( ( O Func S ) X. B ) --> V <-> ( 1st ` E ) : ( ( O Func S ) X. B ) --> ( Base ` T ) ) )
296	294, 295	mpbird 247	. . . . . . . . 9 |- ( ph -> ( 1st ` E ) : ( ( O Func S ) X. B ) --> V )
297	296	fovrnda 6805	. . . . . . . 8 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h ( 1st ` E ) w ) e. V )
298	13, 29, 291, 297, 25	setcinv 16740	. . . . . . 7 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( ( h M w ) ( ( h ( 1st ` Z ) w ) (Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) <-> ( ( h M w ) : ( h ( 1st ` Z ) w ) -1-1-onto-> ( h ( 1st ` E ) w ) /\ ( h N w ) = `' ( h M w ) ) ) )
299	282, 298	mpbird 247	. . . . . 6 |- ( ( ph /\ ( h e. ( O Func S ) /\ w e. B ) ) -> ( h M w ) ( ( h ( 1st ` Z ) w ) (Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) )
300	299	ralrimivva 2971	. . . . 5 |- ( ph -> A. h e. ( O Func S ) A. w e. B ( h M w ) ( ( h ( 1st ` Z ) w ) (Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) )
301		fveq2 6191	. . . . . . . 8 |- ( z = <. h , w >. -> ( M ` z ) = ( M ` <. h , w >. ) )
302		df-ov 6653	. . . . . . . 8 |- ( h M w ) = ( M ` <. h , w >. )
303	301, 302	syl6eqr 2674	. . . . . . 7 |- ( z = <. h , w >. -> ( M ` z ) = ( h M w ) )
304		fveq2 6191	. . . . . . . . 9 |- ( z = <. h , w >. -> ( ( 1st ` Z ) ` z ) = ( ( 1st ` Z ) ` <. h , w >. ) )
305		df-ov 6653	. . . . . . . . 9 |- ( h ( 1st ` Z ) w ) = ( ( 1st ` Z ) ` <. h , w >. )
306	304, 305	syl6eqr 2674	. . . . . . . 8 |- ( z = <. h , w >. -> ( ( 1st ` Z ) ` z ) = ( h ( 1st ` Z ) w ) )
307		fveq2 6191	. . . . . . . . 9 |- ( z = <. h , w >. -> ( ( 1st ` E ) ` z ) = ( ( 1st ` E ) ` <. h , w >. ) )
308		df-ov 6653	. . . . . . . . 9 |- ( h ( 1st ` E ) w ) = ( ( 1st ` E ) ` <. h , w >. )
309	307, 308	syl6eqr 2674	. . . . . . . 8 |- ( z = <. h , w >. -> ( ( 1st ` E ) ` z ) = ( h ( 1st ` E ) w ) )
310	306, 309	oveq12d 6668	. . . . . . 7 |- ( z = <. h , w >. -> ( ( ( 1st ` Z ) ` z ) (Inv ` T ) ( ( 1st ` E ) ` z ) ) = ( ( h ( 1st ` Z ) w ) (Inv ` T ) ( h ( 1st ` E ) w ) ) )
311		fveq2 6191	. . . . . . . 8 |- ( z = <. h , w >. -> ( N ` z ) = ( N ` <. h , w >. ) )
312		df-ov 6653	. . . . . . . 8 |- ( h N w ) = ( N ` <. h , w >. )
313	311, 312	syl6eqr 2674	. . . . . . 7 |- ( z = <. h , w >. -> ( N ` z ) = ( h N w ) )
314	303, 310, 313	breq123d 4667	. . . . . 6 |- ( z = <. h , w >. -> ( ( M ` z ) ( ( ( 1st ` Z ) ` z ) (Inv ` T ) ( ( 1st ` E ) ` z ) ) ( N ` z ) <-> ( h M w ) ( ( h ( 1st ` Z ) w ) (Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) ) )
315	314	ralxp 5263	. . . . 5 |- ( A. z e. ( ( O Func S ) X. B ) ( M ` z ) ( ( ( 1st ` Z ) ` z ) (Inv ` T ) ( ( 1st ` E ) ` z ) ) ( N ` z ) <-> A. h e. ( O Func S ) A. w e. B ( h M w ) ( ( h ( 1st ` Z ) w ) (Inv ` T ) ( h ( 1st ` E ) w ) ) ( h N w ) )
316	300, 315	sylibr 224	. . . 4 |- ( ph -> A. z e. ( ( O Func S ) X. B ) ( M ` z ) ( ( ( 1st ` Z ) ` z ) (Inv ` T ) ( ( 1st ` E ) ` z ) ) ( N ` z ) )
317	316	r19.21bi 2932	. . 3 |- ( ( ph /\ z e. ( ( O Func S ) X. B ) ) -> ( M ` z ) ( ( ( 1st ` Z ) ` z ) (Inv ` T ) ( ( 1st ` E ) ` z ) ) ( N ` z ) )
318	1, 8, 9, 22, 23, 24, 25, 27, 317	invfuc 16634	. 2 |- ( ph -> M ( Z I E ) ( z e. ( ( O Func S ) X. B ) |-> ( N ` z ) ) )
319		fvex 6201	. . . . 5 |- ( ( 1st ` f ) ` x ) e. _V
320	319	mptex 6486	. . . 4 |- ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) e. _V
321	42, 320	fnmpt2i 7239	. . 3 |- N Fn ( ( O Func S ) X. B )
322		dffn5 6241	. . 3 |- ( N Fn ( ( O Func S ) X. B ) <-> N = ( z e. ( ( O Func S ) X. B ) |-> ( N ` z ) ) )
323	321, 322	mpbi 220	. 2 |- N = ( z e. ( ( O Func S ) X. B ) |-> ( N ` z ) )
324	318, 323	syl6breqr 4695	1 |- ( ph -> M ( Z I E ) N )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   u. cun 3572   C_ wss 3574   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   _I cid 5023   X. cxp 5112   `'ccnv 5113   ran crn 5115   |` cres 5116   o. ccom 5118   Rel wrel 5119   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   1stc1st 7166   2ndc2nd 7167  tpos ctpos 7351   Basecbs 15857   Hom chom 15952  compcco 15953   Catccat 16325   Idccid 16326   Hom _f chomf 16327  oppCatcoppc 16371  Invcinv 16405   Func cfunc 16514   o._func ccofu 16516   Nat cnat 16601   FuncCat cfuc 16602   SetCatcsetc 16725   X._c cxpc 16808   1st_F c1stf 16809   2nd_F c2ndf 16810   ⟨,⟩_F cprf 16811   eval_F cevlf 16849  Hom_Fchof 16888  Yoncyon 16889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-fz 12327  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-hom 15966  df-cco 15967  df-cat 16329  df-cid 16330  df-homf 16331  df-comf 16332  df-oppc 16372  df-sect 16407  df-inv 16408  df-ssc 16470  df-resc 16471  df-subc 16472  df-func 16518  df-cofu 16520  df-nat 16603  df-fuc 16604  df-setc 16726  df-xpc 16812  df-1stf 16813  df-2ndf 16814  df-prf 16815  df-evlf 16853  df-curf 16854  df-hof 16890  df-yon 16891

This theorem is referenced by:  yonffthlem  16922  yoneda  16923