fucocolem4

Description: Lemma for fucoco . The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-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)$
Assertion	fucocolem4	$⊢ φ \to (Y P Z) (B) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (A) = (x \in {Base}_{C} ⟼ (U (1^{st} (N) (x)) (⟨1^{st} (K) (1^{st} (L) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (K) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (L) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (R (1^{st} (L) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (L) (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		fucoco.q	$⊢ Q = C FuncCat E$
12		fucoco.oq	$⊢ \underset{˙}{∙} = comp (Q)$
13		eqid	$⊢ C Nat E = C Nat E$
14		eqid	$⊢ {Base}_{C} = {Base}_{C}$
15		eqid	$⊢ comp (E) = comp (E)$
16	9	fveq2d	$⊢ φ \to (X P Y) (A) = (X P Y) (⟨R, S⟩)$
17		df-ov	$⊢ R (X P Y) S = (X P Y) (⟨R, S⟩)$
18	16 17	eqtr4di	$⊢ φ \to (X P Y) (A) = R (X P Y) S$
19	5 2 1 6 7	fuco22nat	$⊢ φ \to R (X P Y) S \in (O (X) (C Nat E) O (Y))$
20	18 19	eqeltrd	$⊢ φ \to (X P Y) (A) \in (O (X) (C Nat E) O (Y))$
21	10	fveq2d	$⊢ φ \to (Y P Z) (B) = (Y P Z) (⟨U, V⟩)$
22		df-ov	$⊢ U (Y P Z) V = (Y P Z) (⟨U, V⟩)$
23	21 22	eqtr4di	$⊢ φ \to (Y P Z) (B) = U (Y P Z) V$
24	5 4 3 7 8	fuco22nat	$⊢ φ \to U (Y P Z) V \in (O (Y) (C Nat E) O (Z))$
25	23 24	eqeltrd	$⊢ φ \to (Y P Z) (B) \in (O (Y) (C Nat E) O (Z))$
26	11 13 14 15 12 20 25	fucco	$⊢ φ \to (Y P Z) (B) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (A) = (x \in {Base}_{C} ⟼ (Y P Z) (B) (x) (⟨1^{st} (O (X)) (x), 1^{st} (O (Y)) (x)⟩ comp (E) 1^{st} (O (Z)) (x)) (X P Y) (A) (x))$
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		relfunc	$⊢ Rel (D Func E)$
35		eqid	$⊢ D Nat E = D Nat E$
36	35	natrcl	$⊢ R \in (F (D Nat E) K) \to (F \in (D Func E) \land K \in (D Func E))$
37	1 36	syl	$⊢ φ \to (F \in (D Func E) \land K \in (D Func E))$
38	37	simpld	$⊢ φ \to F \in (D Func E)$
39		1st2ndbr	$⊢ (Rel (D Func E) \land F \in (D Func E)) \to 1^{st} (F) (D Func E) 2^{nd} (F)$
40	34 38 39	sylancr	$⊢ φ \to 1^{st} (F) (D Func E) 2^{nd} (F)$
41		1st2nd	$⊢ (Rel (D Func E) \land F \in (D Func E)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
42	34 38 41	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
43		1st2nd	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
44	27 31 43	sylancr	$⊢ φ \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
45	42 44	opeq12d	$⊢ φ \to ⟨F, G⟩ = ⟨⟨1^{st} (F), 2^{nd} (F)⟩, ⟨1^{st} (G), 2^{nd} (G)⟩⟩$
46	6 45	eqtrd	$⊢ φ \to X = ⟨⟨1^{st} (F), 2^{nd} (F)⟩, ⟨1^{st} (G), 2^{nd} (G)⟩⟩$
47	5 33 40 46	fuco111	$⊢ φ \to 1^{st} (O (X)) = 1^{st} (F) \circ 1^{st} (G)$
48	47	fveq1d	$⊢ φ \to 1^{st} (O (X)) (x) = (1^{st} (F) \circ 1^{st} (G)) (x)$
49	48	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (X)) (x) = (1^{st} (F) \circ 1^{st} (G)) (x)$
50		eqid	$⊢ {Base}_{D} = {Base}_{D}$
51	14 50 33	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
52	51	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
53		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
54	52 53	fvco3d	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (F) \circ 1^{st} (G)) (x) = 1^{st} (F) (1^{st} (G) (x))$
55	49 54	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (X)) (x) = 1^{st} (F) (1^{st} (G) (x))$
56	30	simprd	$⊢ φ \to L \in (C Func D)$
57		1st2ndbr	$⊢ (Rel (C Func D) \land L \in (C Func D)) \to 1^{st} (L) (C Func D) 2^{nd} (L)$
58	27 56 57	sylancr	$⊢ φ \to 1^{st} (L) (C Func D) 2^{nd} (L)$
59	37	simprd	$⊢ φ \to K \in (D Func E)$
60		1st2ndbr	$⊢ (Rel (D Func E) \land K \in (D Func E)) \to 1^{st} (K) (D Func E) 2^{nd} (K)$
61	34 59 60	sylancr	$⊢ φ \to 1^{st} (K) (D Func E) 2^{nd} (K)$
62		1st2nd	$⊢ (Rel (D Func E) \land K \in (D Func E)) \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
63	34 59 62	sylancr	$⊢ φ \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
64		1st2nd	$⊢ (Rel (C Func D) \land L \in (C Func D)) \to L = ⟨1^{st} (L), 2^{nd} (L)⟩$
65	27 56 64	sylancr	$⊢ φ \to L = ⟨1^{st} (L), 2^{nd} (L)⟩$
66	63 65	opeq12d	$⊢ φ \to ⟨K, L⟩ = ⟨⟨1^{st} (K), 2^{nd} (K)⟩, ⟨1^{st} (L), 2^{nd} (L)⟩⟩$
67	7 66	eqtrd	$⊢ φ \to Y = ⟨⟨1^{st} (K), 2^{nd} (K)⟩, ⟨1^{st} (L), 2^{nd} (L)⟩⟩$
68	5 58 61 67	fuco111	$⊢ φ \to 1^{st} (O (Y)) = 1^{st} (K) \circ 1^{st} (L)$
69	68	fveq1d	$⊢ φ \to 1^{st} (O (Y)) (x) = (1^{st} (K) \circ 1^{st} (L)) (x)$
70	69	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (Y)) (x) = (1^{st} (K) \circ 1^{st} (L)) (x)$
71	14 50 58	funcf1	$⊢ φ \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
72	71	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
73	72 53	fvco3d	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (K) \circ 1^{st} (L)) (x) = 1^{st} (K) (1^{st} (L) (x))$
74	70 73	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (Y)) (x) = 1^{st} (K) (1^{st} (L) (x))$
75	55 74	opeq12d	$⊢ (φ \land x \in {Base}_{C}) \to ⟨1^{st} (O (X)) (x), 1^{st} (O (Y)) (x)⟩ = ⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (L) (x))⟩$
76	28	natrcl	$⊢ V \in (L (C Nat D) N) \to (L \in (C Func D) \land N \in (C Func D))$
77	4 76	syl	$⊢ φ \to (L \in (C Func D) \land N \in (C Func D))$
78	77	simprd	$⊢ φ \to N \in (C Func D)$
79		1st2ndbr	$⊢ (Rel (C Func D) \land N \in (C Func D)) \to 1^{st} (N) (C Func D) 2^{nd} (N)$
80	27 78 79	sylancr	$⊢ φ \to 1^{st} (N) (C Func D) 2^{nd} (N)$
81	35	natrcl	$⊢ U \in (K (D Nat E) M) \to (K \in (D Func E) \land M \in (D Func E))$
82	3 81	syl	$⊢ φ \to (K \in (D Func E) \land M \in (D Func E))$
83	82	simprd	$⊢ φ \to M \in (D Func E)$
84		1st2ndbr	$⊢ (Rel (D Func E) \land M \in (D Func E)) \to 1^{st} (M) (D Func E) 2^{nd} (M)$
85	34 83 84	sylancr	$⊢ φ \to 1^{st} (M) (D Func E) 2^{nd} (M)$
86		1st2nd	$⊢ (Rel (D Func E) \land M \in (D Func E)) \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
87	34 83 86	sylancr	$⊢ φ \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
88		1st2nd	$⊢ (Rel (C Func D) \land N \in (C Func D)) \to N = ⟨1^{st} (N), 2^{nd} (N)⟩$
89	27 78 88	sylancr	$⊢ φ \to N = ⟨1^{st} (N), 2^{nd} (N)⟩$
90	87 89	opeq12d	$⊢ φ \to ⟨M, N⟩ = ⟨⟨1^{st} (M), 2^{nd} (M)⟩, ⟨1^{st} (N), 2^{nd} (N)⟩⟩$
91	8 90	eqtrd	$⊢ φ \to Z = ⟨⟨1^{st} (M), 2^{nd} (M)⟩, ⟨1^{st} (N), 2^{nd} (N)⟩⟩$
92	5 80 85 91	fuco111	$⊢ φ \to 1^{st} (O (Z)) = 1^{st} (M) \circ 1^{st} (N)$
93	92	fveq1d	$⊢ φ \to 1^{st} (O (Z)) (x) = (1^{st} (M) \circ 1^{st} (N)) (x)$
94	93	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (Z)) (x) = (1^{st} (M) \circ 1^{st} (N)) (x)$
95	14 50 80	funcf1	$⊢ φ \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
96	95	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
97	96 53	fvco3d	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (M) \circ 1^{st} (N)) (x) = 1^{st} (M) (1^{st} (N) (x))$
98	94 97	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (Z)) (x) = 1^{st} (M) (1^{st} (N) (x))$
99	75 98	oveq12d	$⊢ (φ \land x \in {Base}_{C}) \to ⟨1^{st} (O (X)) (x), 1^{st} (O (Y)) (x)⟩ comp (E) 1^{st} (O (Z)) (x) = ⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (L) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))$
100	5 7 8 4 3	fuco22a	$⊢ φ \to U (Y P Z) V = (x \in {Base}_{C} ⟼ U (1^{st} (N) (x)) (⟨1^{st} (K) (1^{st} (L) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (K) 1^{st} (N) (x)) (V (x)))$
101	23 100	eqtrd	$⊢ φ \to (Y P Z) (B) = (x \in {Base}_{C} ⟼ U (1^{st} (N) (x)) (⟨1^{st} (K) (1^{st} (L) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (K) 1^{st} (N) (x)) (V (x)))$
102		ovexd	$⊢ (φ \land x \in {Base}_{C}) \to U (1^{st} (N) (x)) (⟨1^{st} (K) (1^{st} (L) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (K) 1^{st} (N) (x)) (V (x)) \in V$
103	101 102	fvmpt2d	$⊢ (φ \land x \in {Base}_{C}) \to (Y P Z) (B) (x) = U (1^{st} (N) (x)) (⟨1^{st} (K) (1^{st} (L) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (K) 1^{st} (N) (x)) (V (x))$
104	5 6 7 2 1	fuco22a	$⊢ φ \to R (X P Y) S = (x \in {Base}_{C} ⟼ R (1^{st} (L) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (L) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x)))$
105	18 104	eqtrd	$⊢ φ \to (X P Y) (A) = (x \in {Base}_{C} ⟼ R (1^{st} (L) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (L) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x)))$
106		ovexd	$⊢ (φ \land x \in {Base}_{C}) \to R (1^{st} (L) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (L) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x)) \in V$
107	105 106	fvmpt2d	$⊢ (φ \land x \in {Base}_{C}) \to (X P Y) (A) (x) = R (1^{st} (L) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (L) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))$
108	99 103 107	oveq123d	$⊢ (φ \land x \in {Base}_{C}) \to (Y P Z) (B) (x) (⟨1^{st} (O (X)) (x), 1^{st} (O (Y)) (x)⟩ comp (E) 1^{st} (O (Z)) (x)) (X P Y) (A) (x) = (U (1^{st} (N) (x)) (⟨1^{st} (K) (1^{st} (L) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (K) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (L) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (R (1^{st} (L) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (L) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x)))$
109	108	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ (Y P Z) (B) (x) (⟨1^{st} (O (X)) (x), 1^{st} (O (Y)) (x)⟩ comp (E) 1^{st} (O (Z)) (x)) (X P Y) (A) (x)) = (x \in {Base}_{C} ⟼ (U (1^{st} (N) (x)) (⟨1^{st} (K) (1^{st} (L) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (K) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (L) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (R (1^{st} (L) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (L) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))))$
110	26 109	eqtrd	$⊢ φ \to (Y P Z) (B) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (A) = (x \in {Base}_{C} ⟼ (U (1^{st} (N) (x)) (⟨1^{st} (K) (1^{st} (L) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (K) 1^{st} (N) (x)) (V (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (K) (1^{st} (L) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (R (1^{st} (L) (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (K) (1^{st} (L) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))))$

Metamath Proof Explorer

Theorem fucocolem4

Proof