fucidcobi

Description: Componentwise functor laws for a correctly typed hom-family into a functor category. The source category T and object assignment O are arbitrary: the identity and composition laws are equivalent to their component equations. No functor law is assumed in the hypotheses. Functor composition is an application in fucoisfunc2 . (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fucidcobi.w	$⊢ W = {Base}_{T}$
	fucidcobi.q	$⊢ Q = C FuncCat E$
	fucidcobi.b	$⊢ B = {Base}_{C}$
	fucidcobi.h	$⊢ H = Hom (T)$
	fucidcobi.i	$⊢ I = Id (T)$
	fucidcobi.j	$⊢ J = Id (Q)$
	fucidcobi.k	$⊢ K = Id (E)$
	fucidcobi.x	$⊢ \underset{˙}{\cdot} = comp (T)$
	fucidcobi.y	No typesetting found for \|- .o. = ( comp ` Q ) with typecode \|-
	fucidcobi.v	$⊢ \underset{˙}{∙} = comp (E)$
	fucidcobi.c	$⊢ φ \to T \in Cat$
	fucidcobi.p	$⊢ φ \to P \in \underset{v \in W \times W}{⨉} ({(O (1^{st} (v)) (C Nat E) O (2^{nd} (v)))}^{H (v)})$
Assertion	fucidcobi	Could not format assertion : No typesetting found for \|- ( ph -> ( 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 \|-

Proof

Step	Hyp	Ref	Expression
1		fucidcobi.w	$⊢ W = {Base}_{T}$
2		fucidcobi.q	$⊢ Q = C FuncCat E$
3		fucidcobi.b	$⊢ B = {Base}_{C}$
4		fucidcobi.h	$⊢ H = Hom (T)$
5		fucidcobi.i	$⊢ I = Id (T)$
6		fucidcobi.j	$⊢ J = Id (Q)$
7		fucidcobi.k	$⊢ K = Id (E)$
8		fucidcobi.x	$⊢ \underset{˙}{\cdot} = comp (T)$
9		fucidcobi.y	Could not format .o. = ( comp ` Q ) : No typesetting found for \|- .o. = ( comp ` Q ) with typecode \|-
10		fucidcobi.v	$⊢ \underset{˙}{∙} = comp (E)$
11		fucidcobi.c	$⊢ φ \to T \in Cat$
12		fucidcobi.p	$⊢ φ \to P \in \underset{v \in W \times W}{⨉} ({(O (1^{st} (v)) (C Nat E) O (2^{nd} (v)))}^{H (v)})$
13		eqid	$⊢ C Nat E = C Nat E$
14	12	adantr	$⊢ (φ \land x \in W) \to P \in \underset{v \in W \times W}{⨉} ({(O (1^{st} (v)) (C Nat E) O (2^{nd} (v)))}^{H (v)})$
15		simpr	$⊢ (φ \land x \in W) \to x \in W$
16	14 15 15	ixpovf	$⊢ (φ \land x \in W) \to (x P x) : x H x ⟶ O (x) (C Nat E) O (x)$
17	11	adantr	$⊢ (φ \land x \in W) \to T \in Cat$
18	1 4 5 17 15	catidcl	$⊢ (φ \land x \in W) \to I (x) \in (x H x)$
19	16 18	ffvelcdmd	$⊢ (φ \land x \in W) \to (x P x) (I (x)) \in (O (x) (C Nat E) O (x))$
20	2 13 3 6 7 19	natideq	$⊢ (φ \land x \in W) \to ((x P x) (I (x)) = J (O (x)) \leftrightarrow \forall t \in B (x P x) (I (x)) (t) = K (1^{st} (O (x)) (t)))$
21		simpl	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to ((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y))$
22	21	simpld	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to (((φ \land x \in W) \land y \in W) \land z \in W)$
23	22	simpld	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to ((φ \land x \in W) \land y \in W)$
24	23	simpld	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to (φ \land x \in W)$
25	24	simpld	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to φ$
26	25 12	syl	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to P \in \underset{v \in W \times W}{⨉} ({(O (1^{st} (v)) (C Nat E) O (2^{nd} (v)))}^{H (v)})$
27	24	simprd	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to x \in W$
28	23	simprd	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to y \in W$
29	26 27 28	ixpovf	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to (x P y) : x H y ⟶ O (x) (C Nat E) O (y)$
30	21	simprd	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to m \in (x H y)$
31	29 30	ffvelcdmd	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to (x P y) (m) \in (O (x) (C Nat E) O (y))$
32	22	simprd	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to z \in W$
33	26 28 32	ixpovf	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to (y P z) : y H z ⟶ O (y) (C Nat E) O (z)$
34		simpr	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to n \in (y H z)$
35	33 34	ffvelcdmd	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to (y P z) (n) \in (O (y) (C Nat E) O (z))$
36	26 27 32	ixpovf	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to (x P z) : x H z ⟶ O (x) (C Nat E) O (z)$
37	25 11	syl	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to T \in Cat$
38	1 4 8 37 27 28 32 30 34	catcocl	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to n (⟨x, y⟩ \underset{˙}{\cdot} z) m \in (x H z)$
39	36 38	ffvelcdmd	$⊢ (((((φ \land x \in W) \land y \in W) \land z \in W) \land m \in (x H y)) \land n \in (y H z)) \to (x P z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) \in (O (x) (C Nat E) O (z))$
40	2 13 3 10 9 31 35 39	natcoeq	Could not format ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ 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. 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 /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ 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. 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 \|-
41	40	ralbidva	Could not format ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ 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. 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 /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ 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. 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 \|-
42	41	ralbidva	Could not format ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ 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. 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 /\ x e. W ) /\ y e. W ) /\ 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. 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 \|-
43	42	ralbidva	Could not format ( ( ( ph /\ x e. W ) /\ 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. 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 /\ x e. W ) /\ 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. 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 \|-
44	43	ralbidva	Could not format ( ( ph /\ x e. W ) -> ( 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. 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 /\ x e. W ) -> ( 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. 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 \|-
45	20 44	anbi12d	Could not format ( ( ph /\ 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. 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 /\ 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. 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 \|-
46	45	ralbidva	Could not format ( ph -> ( 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 -> ( 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 \|-

Metamath Proof Explorer

Theorem fucidcobi

Proof