fucoco

Description: Composition in the source category is mapped to composition in the target. See also fucoco2 . (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fucoco.r	$⊢ φ \to R \in (F (D Nat E) K)$
	fucoco.s	$⊢ φ \to S \in (G (C Nat D) L)$
	fucoco.u	$⊢ φ \to U \in (K (D Nat E) M)$
	fucoco.v	$⊢ φ \to V \in (L (C Nat D) N)$
	fucoco.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fucoco.x	$⊢ φ \to X = ⟨F, G⟩$
	fucoco.y	$⊢ φ \to Y = ⟨K, L⟩$
	fucoco.z	$⊢ φ \to Z = ⟨M, N⟩$
	fucoco.a	$⊢ φ \to A = ⟨R, S⟩$
	fucoco.b	$⊢ φ \to B = ⟨U, V⟩$
	fucoco.q	$⊢ Q = C FuncCat E$
	fucoco.oq	$⊢ \underset{˙}{∙} = comp (Q)$
	fucoco.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
	fucoco.ot	$⊢ \underset{˙}{\cdot} = comp (T)$
Assertion	fucoco	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (Y P Z) (B) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (A)$

Proof

Step	Hyp	Ref	Expression
1		fucoco.r	$⊢ φ \to R \in (F (D Nat E) K)$
2		fucoco.s	$⊢ φ \to S \in (G (C Nat D) L)$
3		fucoco.u	$⊢ φ \to U \in (K (D Nat E) M)$
4		fucoco.v	$⊢ φ \to V \in (L (C Nat D) N)$
5		fucoco.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
6		fucoco.x	$⊢ φ \to X = ⟨F, G⟩$
7		fucoco.y	$⊢ φ \to Y = ⟨K, L⟩$
8		fucoco.z	$⊢ φ \to Z = ⟨M, N⟩$
9		fucoco.a	$⊢ φ \to A = ⟨R, S⟩$
10		fucoco.b	$⊢ φ \to B = ⟨U, V⟩$
11		fucoco.q	$⊢ Q = C FuncCat E$
12		fucoco.oq	$⊢ \underset{˙}{∙} = comp (Q)$
13		fucoco.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
14		fucoco.ot	$⊢ \underset{˙}{\cdot} = comp (T)$
15		eqid	$⊢ C Nat D = C Nat D$
16	15 4	nat1st2nd	$⊢ φ \to V \in (⟨1^{st} (L), 2^{nd} (L)⟩ (C Nat D) ⟨1^{st} (N), 2^{nd} (N)⟩)$
17	16	adantr	$⊢ (φ \land p \in {Base}_{C}) \to V \in (⟨1^{st} (L), 2^{nd} (L)⟩ (C Nat D) ⟨1^{st} (N), 2^{nd} (N)⟩)$
18		eqid	$⊢ D Nat E = D Nat E$
19	18 1	nat1st2nd	$⊢ φ \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ (D Nat E) ⟨1^{st} (K), 2^{nd} (K)⟩)$
20	19	adantr	$⊢ (φ \land p \in {Base}_{C}) \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ (D Nat E) ⟨1^{st} (K), 2^{nd} (K)⟩)$
21		simpr	$⊢ (φ \land p \in {Base}_{C}) \to p \in {Base}_{C}$
22		eqid	$⊢ comp (E) = comp (E)$
23	17 20 21 22	fuco23alem	$⊢ (φ \land p \in {Base}_{C}) \to R (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (F) (1^{st} (N) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (F) 1^{st} (N) (p)) (V (p)) = (1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (K) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) R (1^{st} (L) (p))$
24	23	oveq1d	$⊢ (φ \land p \in {Base}_{C}) \to (R (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (F) (1^{st} (N) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (F) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p)) = ((1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (K) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) R (1^{st} (L) (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p))$
25	24	oveq2d	$⊢ (φ \land p \in {Base}_{C}) \to U (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) ((R (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (F) (1^{st} (N) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (F) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p))) = U (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (((1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (K) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) R (1^{st} (L) (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p)))$
26	1	adantr	$⊢ (φ \land p \in {Base}_{C}) \to R \in (F (D Nat E) K)$
27	2	adantr	$⊢ (φ \land p \in {Base}_{C}) \to S \in (G (C Nat D) L)$
28	3	adantr	$⊢ (φ \land p \in {Base}_{C}) \to U \in (K (D Nat E) M)$
29	4	adantr	$⊢ (φ \land p \in {Base}_{C}) \to V \in (L (C Nat D) N)$
30	18	natrcl	$⊢ R \in (F (D Nat E) K) \to (F \in (D Func E) \land K \in (D Func E))$
31	1 30	syl	$⊢ φ \to (F \in (D Func E) \land K \in (D Func E))$
32	31	simprd	$⊢ φ \to K \in (D Func E)$
33	32	adantr	$⊢ (φ \land p \in {Base}_{C}) \to K \in (D Func E)$
34	15	natrcl	$⊢ S \in (G (C Nat D) L) \to (G \in (C Func D) \land L \in (C Func D))$
35	2 34	syl	$⊢ φ \to (G \in (C Func D) \land L \in (C Func D))$
36	35	simprd	$⊢ φ \to L \in (C Func D)$
37	36	adantr	$⊢ (φ \land p \in {Base}_{C}) \to L \in (C Func D)$
38		eqid	$⊢ {Base}_{D} = {Base}_{D}$
39		eqid	$⊢ Hom (D) = Hom (D)$
40		eqid	$⊢ Hom (E) = Hom (E)$
41		relfunc	$⊢ Rel (D Func E)$
42		1st2ndbr	$⊢ (Rel (D Func E) \land K \in (D Func E)) \to 1^{st} (K) (D Func E) 2^{nd} (K)$
43	41 32 42	sylancr	$⊢ φ \to 1^{st} (K) (D Func E) 2^{nd} (K)$
44	43	adantr	$⊢ (φ \land p \in {Base}_{C}) \to 1^{st} (K) (D Func E) 2^{nd} (K)$
45		eqid	$⊢ {Base}_{C} = {Base}_{C}$
46		relfunc	$⊢ Rel (C Func D)$
47		1st2ndbr	$⊢ (Rel (C Func D) \land L \in (C Func D)) \to 1^{st} (L) (C Func D) 2^{nd} (L)$
48	46 36 47	sylancr	$⊢ φ \to 1^{st} (L) (C Func D) 2^{nd} (L)$
49	45 38 48	funcf1	$⊢ φ \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
50	49	ffvelcdmda	$⊢ (φ \land p \in {Base}_{C}) \to 1^{st} (L) (p) \in {Base}_{D}$
51	15	natrcl	$⊢ V \in (L (C Nat D) N) \to (L \in (C Func D) \land N \in (C Func D))$
52	4 51	syl	$⊢ φ \to (L \in (C Func D) \land N \in (C Func D))$
53	52	simprd	$⊢ φ \to N \in (C Func D)$
54		1st2ndbr	$⊢ (Rel (C Func D) \land N \in (C Func D)) \to 1^{st} (N) (C Func D) 2^{nd} (N)$
55	46 53 54	sylancr	$⊢ φ \to 1^{st} (N) (C Func D) 2^{nd} (N)$
56	45 38 55	funcf1	$⊢ φ \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
57	56	ffvelcdmda	$⊢ (φ \land p \in {Base}_{C}) \to 1^{st} (N) (p) \in {Base}_{D}$
58	38 39 40 44 50 57	funcf2	$⊢ (φ \land p \in {Base}_{C}) \to (1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) : 1^{st} (L) (p) Hom (D) 1^{st} (N) (p) ⟶ 1^{st} (K) (1^{st} (L) (p)) Hom (E) 1^{st} (K) (1^{st} (N) (p))$
59	15 17 45 39 21	natcl	$⊢ (φ \land p \in {Base}_{C}) \to V (p) \in (1^{st} (L) (p) Hom (D) 1^{st} (N) (p))$
60	58 59	ffvelcdmd	$⊢ (φ \land p \in {Base}_{C}) \to (1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p)) \in (1^{st} (K) (1^{st} (L) (p)) Hom (E) 1^{st} (K) (1^{st} (N) (p)))$
61	18 20 38 40 50	natcl	$⊢ (φ \land p \in {Base}_{C}) \to R (1^{st} (L) (p)) \in (1^{st} (F) (1^{st} (L) (p)) Hom (E) 1^{st} (K) (1^{st} (L) (p)))$
62	26 27 28 29 21 33 37 60 61	fucocolem1	$⊢ (φ \land p \in {Base}_{C}) \to (U (1^{st} (N) (p)) (⟨1^{st} (K) (1^{st} (L) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (L) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (R (1^{st} (L) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (L) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p))) = U (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (((1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (K) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) R (1^{st} (L) (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p)))$
63	25 62	eqtr4d	$⊢ (φ \land p \in {Base}_{C}) \to U (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) ((R (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (F) (1^{st} (N) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (F) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p))) = (U (1^{st} (N) (p)) (⟨1^{st} (K) (1^{st} (L) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (L) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (R (1^{st} (L) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (L) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p)))$
64	63	mpteq2dva	$⊢ φ \to (p \in {Base}_{C} ⟼ U (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) ((R (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (F) (1^{st} (N) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (F) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p)))) = (p \in {Base}_{C} ⟼ (U (1^{st} (N) (p)) (⟨1^{st} (K) (1^{st} (L) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (L) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (R (1^{st} (L) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (L) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p))))$
65		eqid	$⊢ comp (D) = comp (D)$
66	1 2 3 4 5 6 7 8 9 10 13 14 65	fucocolem3	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (p \in {Base}_{C} ⟼ U (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) ((R (1^{st} (N) (p)) (⟨1^{st} (F) (1^{st} (L) (p)), 1^{st} (F) (1^{st} (N) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (F) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (N) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p))))$
67	1 2 3 4 5 6 7 8 9 10 11 12	fucocolem4	$⊢ φ \to (Y P Z) (B) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (A) = (p \in {Base}_{C} ⟼ (U (1^{st} (N) (p)) (⟨1^{st} (K) (1^{st} (L) (p)), 1^{st} (K) (1^{st} (N) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (1^{st} (L) (p) 2^{nd} (K) 1^{st} (N) (p)) (V (p))) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (K) (1^{st} (L) (p))⟩ comp (E) 1^{st} (M) (1^{st} (N) (p))) (R (1^{st} (L) (p)) (⟨1^{st} (F) (1^{st} (G) (p)), 1^{st} (F) (1^{st} (L) (p))⟩ comp (E) 1^{st} (K) (1^{st} (L) (p))) (1^{st} (G) (p) 2^{nd} (F) 1^{st} (L) (p)) (S (p))))$
68	64 66 67	3eqtr4d	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (Y P Z) (B) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (A)$

Metamath Proof Explorer

Theorem fucoco

Proof