Theorem fucoisfunc2lem2

Description: Lemma for fucoisfunc2 . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fucoisfunc.w	$$⊢W=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
	fucoisfunc2lem1.o	$$⊢O={{\circ }_{\mathrm{func}}\upharpoonright }_W$$
	fucoisfunc2lem1.b	$$⊢B={\mathrm{Base}}_C$$
	fucoisfunc2lem1.r	$$⊢R=\mathrm{Hom}\left(C\right)$$
	fucoisfunc2lem1.s	$$⊢S=\mathrm{Hom}\left(E\right)$$
	fucoisfunc2lem1.v	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
	fucoisfunc2.t	$$⊢T=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
	fucoisfunc2.q	$$⊢Q=C\mathrm{FuncCat}E$$
	fucoisfunc2.h	$$⊢H=\mathrm{Hom}\left(T\right)$$
	fucoisfunc2.i	$$⊢I=\mathrm{Id}\left(T\right)$$
	fucoisfunc2.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(T\right)$$
	fucoisfunc2.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	fucoisfunc2.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	fucoisfunc2.e	$$⊢\phi \to E\in \mathrm{Cat}$$
	fucoisfunc2.k	$$⊢K=\mathrm{Id}\left(E\right)$$
	fucoisfunc2lem2.j	$$⊢J=\mathrm{Id}\left(Q\right)$$
	fucoisfunc2lem2.y	No typesetting found for |- .o. = ( comp ` Q ) with typecode |-
Assertion	fucoisfunc2lem2	$$⊢\phi \to \left(O\left(T\mathrm{Func}Q\right)P\leftrightarrow \left(\left(P=\left(u\in W,v\in W⟼uPv\right)\wedge \forall m\in W\forall n\in W\left(mPn=\left(b\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right),a\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)⟼b\left(mPn\right)a\right)\wedge \forall p\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right)\forall q\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)\left(p\left(mPn\right)q=\left(x\in B⟼\left(p\left(mPn\right)q\right)\left(x\right)\right)\wedge \forall x\in B\left(p\left(mPn\right)q\right)\left(x\right)\in \left(1^{st}\left(O\left(m\right)\right)\left(x\right)S{1}^{st}\left(O\left(n\right)\right)\left(x\right)\right)\wedge \forall x\in B\forall y\in B\forall h\in \left(xRy\right)\left(p\left(mPn\right)q\right)\left(y\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(m\right)\right)\left(y\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(x{2}^{nd}\left(O\left(m\right)\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(O\left(n\right)\right)y\right)\left(h\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(n\right)\right)\left(x\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(p\left(mPn\right)q\right)\left(x\right)\right)\right)\right)\wedge \forall x\in W\left(\forall t\in B\left(xPx\right)\left(I\left(x\right)\right)\left(t\right)=K\left(1^{st}\left(O\left(x\right)\right)\left(t\right)\right)\wedge \forall y\in W\forall z\in W\forall m\in \left(xHy\right)\forall n\in \left(yHz\right)\forall t\in B\left(xPz\right)\left(n\left(⟨x,y⟩\underset{\dot{}}{·}z\right)m\right)\left(t\right)=\left(yPz\right)\left(n\right)\left(t\right)\left(⟨1^{st}\left(O\left(x\right)\right)\left(t\right),1^{st}\left(O\left(y\right)\right)\left(t\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(z\right)\right)\left(t\right)\right)\left(xPy\right)\left(m\right)\left(t\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	$$⊢W=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
2		fucoisfunc2lem1.o	$$⊢O={{\circ }_{\mathrm{func}}\upharpoonright }_W$$
3		fucoisfunc2lem1.b	$$⊢B={\mathrm{Base}}_C$$
4		fucoisfunc2lem1.r	$$⊢R=\mathrm{Hom}\left(C\right)$$
5		fucoisfunc2lem1.s	$$⊢S=\mathrm{Hom}\left(E\right)$$
6		fucoisfunc2lem1.v	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(E\right)$$
7		fucoisfunc2.t	$$⊢T=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
8		fucoisfunc2.q	$$⊢Q=C\mathrm{FuncCat}E$$
9		fucoisfunc2.h	$$⊢H=\mathrm{Hom}\left(T\right)$$
10		fucoisfunc2.i	$$⊢I=\mathrm{Id}\left(T\right)$$
11		fucoisfunc2.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(T\right)$$
12		fucoisfunc2.c	$$⊢\phi \to C\in \mathrm{Cat}$$
13		fucoisfunc2.d	$$⊢\phi \to D\in \mathrm{Cat}$$
14		fucoisfunc2.e	$$⊢\phi \to E\in \mathrm{Cat}$$
15		fucoisfunc2.k	$$⊢K=\mathrm{Id}\left(E\right)$$
16		fucoisfunc2lem2.j	$$⊢J=\mathrm{Id}\left(Q\right)$$
17		fucoisfunc2lem2.y	Could not format .o. = ( comp ` Q ) : No typesetting found for |- .o. = ( comp ` Q ) with typecode |-
18	1 7 8 2 9 10 16 11 17 12 13 14	fucoisfunc	Could not format ( ph -> ( O ( T Func Q ) P <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( O ( T Func Q ) P <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) with typecode |-
19	7	fveq2i	$$⊢\mathrm{Hom}\left(T\right)=\mathrm{Hom}\left(\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)\right)$$
20	9 19	eqtri	$$⊢H=\mathrm{Hom}\left(\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)\right)$$
21	1 20	fucofulem2	$$⊢P\in \underset{w\in W\times W}{⨉}\left({\left(O\left(1^{st}\left(w\right)\right)\left(C\mathrm{Nat}E\right)O\left(2^{nd}\left(w\right)\right)\right)}^{H\left(w\right)}\right)\leftrightarrow \left(P=\left(u\in W,v\in W⟼uPv\right)\wedge \forall m\in W\forall n\in W\left(mPn=\left(b\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right),a\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)⟼b\left(mPn\right)a\right)\wedge \forall p\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right)\forall q\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)p\left(mPn\right)q\in \left(O\left(m\right)\left(C\mathrm{Nat}E\right)O\left(n\right)\right)\right)\right)$$
22	21	anbi1i	Could not format ( ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) : No typesetting found for |- ( ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) with typecode |-
23	18 22	bitr4di	Could not format ( ph -> ( O ( T Func Q ) P <-> ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( O ( T Func Q ) P <-> ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) with typecode |-
24	7	xpcfucbas	$$⊢\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)={\mathrm{Base}}_T$$
25	1 24	eqtri	$$⊢W={\mathrm{Base}}_T$$
26		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
27	26 13 14	fuccat	$$⊢\phi \to D\mathrm{FuncCat}E\in \mathrm{Cat}$$
28		eqid	$$⊢C\mathrm{FuncCat}D=C\mathrm{FuncCat}D$$
29	28 12 13	fuccat	$$⊢\phi \to C\mathrm{FuncCat}D\in \mathrm{Cat}$$
30	7 27 29	xpccat	$$⊢\phi \to T\in \mathrm{Cat}$$
31	30	adantr	$$⊢\left(\phi \wedge P\in \underset{w\in W\times W}{⨉}\left({\left(O\left(1^{st}\left(w\right)\right)\left(C\mathrm{Nat}E\right)O\left(2^{nd}\left(w\right)\right)\right)}^{H\left(w\right)}\right)\right)\to T\in \mathrm{Cat}$$
32		simpr	$$⊢\left(\phi \wedge P\in \underset{w\in W\times W}{⨉}\left({\left(O\left(1^{st}\left(w\right)\right)\left(C\mathrm{Nat}E\right)O\left(2^{nd}\left(w\right)\right)\right)}^{H\left(w\right)}\right)\right)\to P\in \underset{w\in W\times W}{⨉}\left({\left(O\left(1^{st}\left(w\right)\right)\left(C\mathrm{Nat}E\right)O\left(2^{nd}\left(w\right)\right)\right)}^{H\left(w\right)}\right)$$
33	25 8 3 9 10 16 15 11 17 6 31 32	fucidcobi	Could not format ( ( ph /\ P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) ) -> ( A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) <-> A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) : No typesetting found for |- ( ( ph /\ P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) ) -> ( A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) <-> A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) with typecode |-
34	33	pm5.32da	Could not format ( ph -> ( ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) ) with typecode |-
35	23 34	bitrd	$$⊢\phi \to \left(O\left(T\mathrm{Func}Q\right)P\leftrightarrow \left(P\in \underset{w\in W\times W}{⨉}\left({\left(O\left(1^{st}\left(w\right)\right)\left(C\mathrm{Nat}E\right)O\left(2^{nd}\left(w\right)\right)\right)}^{H\left(w\right)}\right)\wedge \forall x\in W\left(\forall t\in B\left(xPx\right)\left(I\left(x\right)\right)\left(t\right)=K\left(1^{st}\left(O\left(x\right)\right)\left(t\right)\right)\wedge \forall y\in W\forall z\in W\forall m\in \left(xHy\right)\forall n\in \left(yHz\right)\forall t\in B\left(xPz\right)\left(n\left(⟨x,y⟩\underset{\dot{}}{·}z\right)m\right)\left(t\right)=\left(yPz\right)\left(n\right)\left(t\right)\left(⟨1^{st}\left(O\left(x\right)\right)\left(t\right),1^{st}\left(O\left(y\right)\right)\left(t\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(z\right)\right)\left(t\right)\right)\left(xPy\right)\left(m\right)\left(t\right)\right)\right)\right)$$
36	1 2 3 4 5 6	fucoisfunc2lem1	$$⊢\left(P=\left(u\in W,v\in W⟼uPv\right)\wedge \forall m\in W\forall n\in W\left(mPn=\left(b\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right),a\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)⟼b\left(mPn\right)a\right)\wedge \forall p\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right)\forall q\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)p\left(mPn\right)q\in \left(O\left(m\right)\left(C\mathrm{Nat}E\right)O\left(n\right)\right)\right)\right)\leftrightarrow \left(P=\left(u\in W,v\in W⟼uPv\right)\wedge \forall m\in W\forall n\in W\left(mPn=\left(b\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right),a\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)⟼b\left(mPn\right)a\right)\wedge \forall p\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right)\forall q\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)\left(p\left(mPn\right)q=\left(x\in B⟼\left(p\left(mPn\right)q\right)\left(x\right)\right)\wedge \forall x\in B\left(p\left(mPn\right)q\right)\left(x\right)\in \left(1^{st}\left(O\left(m\right)\right)\left(x\right)S{1}^{st}\left(O\left(n\right)\right)\left(x\right)\right)\wedge \forall x\in B\forall y\in B\forall h\in \left(xRy\right)\left(p\left(mPn\right)q\right)\left(y\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(m\right)\right)\left(y\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(x{2}^{nd}\left(O\left(m\right)\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(O\left(n\right)\right)y\right)\left(h\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(n\right)\right)\left(x\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(p\left(mPn\right)q\right)\left(x\right)\right)\right)\right)$$
37	21 36	bitri	$$⊢P\in \underset{w\in W\times W}{⨉}\left({\left(O\left(1^{st}\left(w\right)\right)\left(C\mathrm{Nat}E\right)O\left(2^{nd}\left(w\right)\right)\right)}^{H\left(w\right)}\right)\leftrightarrow \left(P=\left(u\in W,v\in W⟼uPv\right)\wedge \forall m\in W\forall n\in W\left(mPn=\left(b\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right),a\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)⟼b\left(mPn\right)a\right)\wedge \forall p\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right)\forall q\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)\left(p\left(mPn\right)q=\left(x\in B⟼\left(p\left(mPn\right)q\right)\left(x\right)\right)\wedge \forall x\in B\left(p\left(mPn\right)q\right)\left(x\right)\in \left(1^{st}\left(O\left(m\right)\right)\left(x\right)S{1}^{st}\left(O\left(n\right)\right)\left(x\right)\right)\wedge \forall x\in B\forall y\in B\forall h\in \left(xRy\right)\left(p\left(mPn\right)q\right)\left(y\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(m\right)\right)\left(y\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(x{2}^{nd}\left(O\left(m\right)\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(O\left(n\right)\right)y\right)\left(h\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(n\right)\right)\left(x\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(p\left(mPn\right)q\right)\left(x\right)\right)\right)\right)$$
38	37	anbi1i	$$⊢\left(P\in \underset{w\in W\times W}{⨉}\left({\left(O\left(1^{st}\left(w\right)\right)\left(C\mathrm{Nat}E\right)O\left(2^{nd}\left(w\right)\right)\right)}^{H\left(w\right)}\right)\wedge \forall x\in W\left(\forall t\in B\left(xPx\right)\left(I\left(x\right)\right)\left(t\right)=K\left(1^{st}\left(O\left(x\right)\right)\left(t\right)\right)\wedge \forall y\in W\forall z\in W\forall m\in \left(xHy\right)\forall n\in \left(yHz\right)\forall t\in B\left(xPz\right)\left(n\left(⟨x,y⟩\underset{\dot{}}{·}z\right)m\right)\left(t\right)=\left(yPz\right)\left(n\right)\left(t\right)\left(⟨1^{st}\left(O\left(x\right)\right)\left(t\right),1^{st}\left(O\left(y\right)\right)\left(t\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(z\right)\right)\left(t\right)\right)\left(xPy\right)\left(m\right)\left(t\right)\right)\right)\leftrightarrow \left(\left(P=\left(u\in W,v\in W⟼uPv\right)\wedge \forall m\in W\forall n\in W\left(mPn=\left(b\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right),a\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)⟼b\left(mPn\right)a\right)\wedge \forall p\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right)\forall q\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)\left(p\left(mPn\right)q=\left(x\in B⟼\left(p\left(mPn\right)q\right)\left(x\right)\right)\wedge \forall x\in B\left(p\left(mPn\right)q\right)\left(x\right)\in \left(1^{st}\left(O\left(m\right)\right)\left(x\right)S{1}^{st}\left(O\left(n\right)\right)\left(x\right)\right)\wedge \forall x\in B\forall y\in B\forall h\in \left(xRy\right)\left(p\left(mPn\right)q\right)\left(y\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(m\right)\right)\left(y\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(x{2}^{nd}\left(O\left(m\right)\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(O\left(n\right)\right)y\right)\left(h\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(n\right)\right)\left(x\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(p\left(mPn\right)q\right)\left(x\right)\right)\right)\right)\wedge \forall x\in W\left(\forall t\in B\left(xPx\right)\left(I\left(x\right)\right)\left(t\right)=K\left(1^{st}\left(O\left(x\right)\right)\left(t\right)\right)\wedge \forall y\in W\forall z\in W\forall m\in \left(xHy\right)\forall n\in \left(yHz\right)\forall t\in B\left(xPz\right)\left(n\left(⟨x,y⟩\underset{\dot{}}{·}z\right)m\right)\left(t\right)=\left(yPz\right)\left(n\right)\left(t\right)\left(⟨1^{st}\left(O\left(x\right)\right)\left(t\right),1^{st}\left(O\left(y\right)\right)\left(t\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(z\right)\right)\left(t\right)\right)\left(xPy\right)\left(m\right)\left(t\right)\right)\right)$$
39	35 38	bitrdi	$$⊢\phi \to \left(O\left(T\mathrm{Func}Q\right)P\leftrightarrow \left(\left(P=\left(u\in W,v\in W⟼uPv\right)\wedge \forall m\in W\forall n\in W\left(mPn=\left(b\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right),a\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)⟼b\left(mPn\right)a\right)\wedge \forall p\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right)\forall q\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)\left(p\left(mPn\right)q=\left(x\in B⟼\left(p\left(mPn\right)q\right)\left(x\right)\right)\wedge \forall x\in B\left(p\left(mPn\right)q\right)\left(x\right)\in \left(1^{st}\left(O\left(m\right)\right)\left(x\right)S{1}^{st}\left(O\left(n\right)\right)\left(x\right)\right)\wedge \forall x\in B\forall y\in B\forall h\in \left(xRy\right)\left(p\left(mPn\right)q\right)\left(y\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(m\right)\right)\left(y\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(x{2}^{nd}\left(O\left(m\right)\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(O\left(n\right)\right)y\right)\left(h\right)\left(⟨1^{st}\left(O\left(m\right)\right)\left(x\right),1^{st}\left(O\left(n\right)\right)\left(x\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(n\right)\right)\left(y\right)\right)\left(p\left(mPn\right)q\right)\left(x\right)\right)\right)\right)\wedge \forall x\in W\left(\forall t\in B\left(xPx\right)\left(I\left(x\right)\right)\left(t\right)=K\left(1^{st}\left(O\left(x\right)\right)\left(t\right)\right)\wedge \forall y\in W\forall z\in W\forall m\in \left(xHy\right)\forall n\in \left(yHz\right)\forall t\in B\left(xPz\right)\left(n\left(⟨x,y⟩\underset{\dot{}}{·}z\right)m\right)\left(t\right)=\left(yPz\right)\left(n\right)\left(t\right)\left(⟨1^{st}\left(O\left(x\right)\right)\left(t\right),1^{st}\left(O\left(y\right)\right)\left(t\right)⟩\underset{\dot{}}{\bullet }{1}^{st}\left(O\left(z\right)\right)\left(t\right)\right)\left(xPy\right)\left(m\right)\left(t\right)\right)\right)\right)$$