Theorem fucoisfunc2lem1

Description: Lemma for fucoisfunc2lem2 . An equivalence that expands the transformation outputs of a composition-shaped hom-family into exact component functions, component typing, and naturality. The component values are arbitrary; no canonical value is imposed. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fucoisfunc.w	|- W = ( ( D Func E ) X. ( C Func D ) )
	fucoisfunc2lem1.o	|- O = ( o.func |` W )
	fucoisfunc2lem1.b	|- B = ( Base ` C )
	fucoisfunc2lem1.r	|- R = ( Hom ` C )
	fucoisfunc2lem1.s	|- S = ( Hom ` E )
	fucoisfunc2lem1.v	|- .xb = ( comp ` E )
Assertion	fucoisfunc2lem1	|- ( ( 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 ) ) ) ) <-> ( 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 ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	|- W = ( ( D Func E ) X. ( C Func D ) )
2		fucoisfunc2lem1.o	|- O = ( o.func |` W )
3		fucoisfunc2lem1.b	|- B = ( Base ` C )
4		fucoisfunc2lem1.r	|- R = ( Hom ` C )
5		fucoisfunc2lem1.s	|- S = ( Hom ` E )
6		fucoisfunc2lem1.v	|- .xb = ( comp ` E )
7		eqid	|- ( C Nat E ) = ( C Nat E )
8		rescofuf	|- ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E )
9	1	reseq2i	|- ( o.func |` W ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) )
10	2 9	eqtri	|- O = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) )
11	10 1	feq12i	|- ( O : W --> ( C Func E ) <-> ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E ) )
12	8 11	mpbir	|- O : W --> ( C Func E )
13	12	a1i	|- ( ( ( T. /\ m e. W ) /\ n e. W ) -> O : W --> ( C Func E ) )
14		simplr	|- ( ( ( T. /\ m e. W ) /\ n e. W ) -> m e. W )
15	13 14	ffvelcdmd	|- ( ( ( T. /\ m e. W ) /\ n e. W ) -> ( O ` m ) e. ( C Func E ) )
16		simpr	|- ( ( ( T. /\ m e. W ) /\ n e. W ) -> n e. W )
17	13 16	ffvelcdmd	|- ( ( ( T. /\ m e. W ) /\ n e. W ) -> ( O ` n ) e. ( C Func E ) )
18	7 3 4 5 6 15 17	isnat3	|- ( ( ( T. /\ m e. W ) /\ n e. W ) -> ( ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) <-> ( ( p ( m P n ) q ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) )
19	18	2ralbidv	|- ( ( ( T. /\ m e. W ) /\ n e. W ) -> ( 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. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( ( p ( m P n ) q ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) )
20	19	anbi2d	|- ( ( ( T. /\ m e. W ) /\ 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 ) ) ) <-> ( ( 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 ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) )
21	20	ralbidva	|- ( ( T. /\ 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. 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 ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) )
22	21	ralbidva	|- ( T. -> ( 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. 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 ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) )
23	22	anbi2d	|- ( T. -> ( ( 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 ) ) ) ) <-> ( 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 ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) ) )
24	23	mptru	|- ( ( 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 ) ) ) ) <-> ( 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 ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) )