fucocolem3

Description: Lemma for fucoco . The composed natural transformations are mapped to composition of 4 natural transformations. (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⟩$
	fucocolem2.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
	fucocolem2.ot	$⊢ \underset{˙}{\cdot} = comp (T)$
	fucocolem2.od	$⊢ \underset{˙}{*} = comp (D)$
Assertion	fucocolem3	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (x \in {Base}_{C} ⟼ U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))))$

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		fucocolem2.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
12		fucocolem2.ot	$⊢ \underset{˙}{\cdot} = comp (T)$
13		fucocolem2.od	$⊢ \underset{˙}{*} = comp (D)$
14	1 2 3 4 5 6 7 8 9 10 11 12 13	fucocolem2	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (x \in {Base}_{C} ⟼ (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x)))$
15		eqid	$⊢ {Base}_{D} = {Base}_{D}$
16		eqid	$⊢ Hom (D) = Hom (D)$
17		eqid	$⊢ comp (E) = comp (E)$
18		relfunc	$⊢ Rel (D Func E)$
19		eqid	$⊢ D Nat E = D Nat E$
20	19	natrcl	$⊢ R \in (F (D Nat E) K) \to (F \in (D Func E) \land K \in (D Func E))$
21	1 20	syl	$⊢ φ \to (F \in (D Func E) \land K \in (D Func E))$
22	21	simpld	$⊢ φ \to F \in (D Func E)$
23		1st2ndbr	$⊢ (Rel (D Func E) \land F \in (D Func E)) \to 1^{st} (F) (D Func E) 2^{nd} (F)$
24	18 22 23	sylancr	$⊢ φ \to 1^{st} (F) (D Func E) 2^{nd} (F)$
25	24	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (D Func E) 2^{nd} (F)$
26		eqid	$⊢ {Base}_{C} = {Base}_{C}$
27		relfunc	$⊢ Rel (C Func D)$
28		eqid	$⊢ C Nat D = C Nat D$
29	28	natrcl	$⊢ S \in (G (C Nat D) L) \to (G \in (C Func D) \land L \in (C Func D))$
30	2 29	syl	$⊢ φ \to (G \in (C Func D) \land L \in (C Func D))$
31	30	simpld	$⊢ φ \to G \in (C Func D)$
32		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
33	27 31 32	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
34	26 15 33	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
35	34	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) \in {Base}_{D}$
36	30	simprd	$⊢ φ \to L \in (C Func D)$
37		1st2ndbr	$⊢ (Rel (C Func D) \land L \in (C Func D)) \to 1^{st} (L) (C Func D) 2^{nd} (L)$
38	27 36 37	sylancr	$⊢ φ \to 1^{st} (L) (C Func D) 2^{nd} (L)$
39	26 15 38	funcf1	$⊢ φ \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
40	39	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (L) (x) \in {Base}_{D}$
41	28	natrcl	$⊢ V \in (L (C Nat D) N) \to (L \in (C Func D) \land N \in (C Func D))$
42	4 41	syl	$⊢ φ \to (L \in (C Func D) \land N \in (C Func D))$
43	42	simprd	$⊢ φ \to N \in (C Func D)$
44		1st2ndbr	$⊢ (Rel (C Func D) \land N \in (C Func D)) \to 1^{st} (N) (C Func D) 2^{nd} (N)$
45	27 43 44	sylancr	$⊢ φ \to 1^{st} (N) (C Func D) 2^{nd} (N)$
46	26 15 45	funcf1	$⊢ φ \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
47	46	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (N) (x) \in {Base}_{D}$
48	28 2	nat1st2nd	$⊢ φ \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ (C Nat D) ⟨1^{st} (L), 2^{nd} (L)⟩)$
49	48	adantr	$⊢ (φ \land x \in {Base}_{C}) \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ (C Nat D) ⟨1^{st} (L), 2^{nd} (L)⟩)$
50		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
51	28 49 26 16 50	natcl	$⊢ (φ \land x \in {Base}_{C}) \to S (x) \in (1^{st} (G) (x) Hom (D) 1^{st} (L) (x))$
52	28 4	nat1st2nd	$⊢ φ \to V \in (⟨1^{st} (L), 2^{nd} (L)⟩ (C Nat D) ⟨1^{st} (N), 2^{nd} (N)⟩)$
53	52	adantr	$⊢ (φ \land x \in {Base}_{C}) \to V \in (⟨1^{st} (L), 2^{nd} (L)⟩ (C Nat D) ⟨1^{st} (N), 2^{nd} (N)⟩)$
54	28 53 26 16 50	natcl	$⊢ (φ \land x \in {Base}_{C}) \to V (x) \in (1^{st} (L) (x) Hom (D) 1^{st} (N) (x))$
55	15 16 13 17 25 35 40 47 51 54	funcco	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x)) = (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (F) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))$
56	55	oveq2d	$⊢ (φ \land x \in {Base}_{C}) \to (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x)) = (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (F) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x)))$
57	1	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R \in (F (D Nat E) K)$
58	2	adantr	$⊢ (φ \land x \in {Base}_{C}) \to S \in (G (C Nat D) L)$
59	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to U \in (K (D Nat E) M)$
60	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to V \in (L (C Nat D) N)$
61	22	adantr	$⊢ (φ \land x \in {Base}_{C}) \to F \in (D Func E)$
62	43	adantr	$⊢ (φ \land x \in {Base}_{C}) \to N \in (C Func D)$
63	19 1	nat1st2nd	$⊢ φ \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ (D Nat E) ⟨1^{st} (K), 2^{nd} (K)⟩)$
64	63	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ (D Nat E) ⟨1^{st} (K), 2^{nd} (K)⟩)$
65		eqid	$⊢ Hom (E) = Hom (E)$
66	19 64 15 65 47	natcl	$⊢ (φ \land x \in {Base}_{C}) \to R (1^{st} (N) (x)) \in (1^{st} (F) (1^{st} (N) (x)) Hom (E) 1^{st} (K) (1^{st} (N) (x)))$
67	15 16 65 25 40 47	funcf2	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) : 1^{st} (L) (x) Hom (D) 1^{st} (N) (x) ⟶ 1^{st} (F) (1^{st} (L) (x)) Hom (E) 1^{st} (F) (1^{st} (N) (x))$
68	67 54	ffvelcdmd	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x)) \in (1^{st} (F) (1^{st} (L) (x)) Hom (E) 1^{st} (F) (1^{st} (N) (x)))$
69	57 58 59 60 50 61 62 66 68	fucocolem1	$⊢ (φ \land x \in {Base}_{C}) \to (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (F) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))) = U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x)))$
70	56 69	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x)) = U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x)))$
71	70	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x))) = (x \in {Base}_{C} ⟼ U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))))$
72	14 71	eqtrd	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (x \in {Base}_{C} ⟼ U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))))$

Metamath Proof Explorer

Theorem fucocolem3

Proof