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		eqid	$⊢ C Nat D = C Nat D$
28	27	natrcl	$⊢ S \in (G (C Nat D) L) \to (G \in (C Func D) \land L \in (C Func D))$
29	2 28	syl	$⊢ φ \to (G \in (C Func D) \land L \in (C Func D))$
30	29	simpld	$⊢ φ \to G \in (C Func D)$
31	30	func1st2nd	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
32		eqid	$⊢ D Nat E = D Nat E$
33	32	natrcl	$⊢ R \in (F (D Nat E) K) \to (F \in (D Func E) \land K \in (D Func E))$
34	1 33	syl	$⊢ φ \to (F \in (D Func E) \land K \in (D Func E))$
35	34	simpld	$⊢ φ \to F \in (D Func E)$
36	35	func1st2nd	$⊢ φ \to 1^{st} (F) (D Func E) 2^{nd} (F)$
37		relfunc	$⊢ Rel (D Func E)$
38		1st2nd	$⊢ (Rel (D Func E) \land F \in (D Func E)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
39	37 35 38	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
40		relfunc	$⊢ Rel (C Func D)$
41		1st2nd	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
42	40 30 41	sylancr	$⊢ φ \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
43	39 42	opeq12d	$⊢ φ \to ⟨F, G⟩ = ⟨⟨1^{st} (F), 2^{nd} (F)⟩, ⟨1^{st} (G), 2^{nd} (G)⟩⟩$
44	6 43	eqtrd	$⊢ φ \to X = ⟨⟨1^{st} (F), 2^{nd} (F)⟩, ⟨1^{st} (G), 2^{nd} (G)⟩⟩$
45	5 31 36 44	fuco111	$⊢ φ \to 1^{st} (O (X)) = 1^{st} (F) \circ 1^{st} (G)$
46	45	fveq1d	$⊢ φ \to 1^{st} (O (X)) (x) = (1^{st} (F) \circ 1^{st} (G)) (x)$
47	46	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (X)) (x) = (1^{st} (F) \circ 1^{st} (G)) (x)$
48		eqid	$⊢ {Base}_{D} = {Base}_{D}$
49	14 48 31	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
50	49	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
51		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
52	50 51	fvco3d	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (F) \circ 1^{st} (G)) (x) = 1^{st} (F) (1^{st} (G) (x))$
53	47 52	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (X)) (x) = 1^{st} (F) (1^{st} (G) (x))$
54	29	simprd	$⊢ φ \to L \in (C Func D)$
55	54	func1st2nd	$⊢ φ \to 1^{st} (L) (C Func D) 2^{nd} (L)$
56	34	simprd	$⊢ φ \to K \in (D Func E)$
57	56	func1st2nd	$⊢ φ \to 1^{st} (K) (D Func E) 2^{nd} (K)$
58		1st2nd	$⊢ (Rel (D Func E) \land K \in (D Func E)) \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
59	37 56 58	sylancr	$⊢ φ \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
60		1st2nd	$⊢ (Rel (C Func D) \land L \in (C Func D)) \to L = ⟨1^{st} (L), 2^{nd} (L)⟩$
61	40 54 60	sylancr	$⊢ φ \to L = ⟨1^{st} (L), 2^{nd} (L)⟩$
62	59 61	opeq12d	$⊢ φ \to ⟨K, L⟩ = ⟨⟨1^{st} (K), 2^{nd} (K)⟩, ⟨1^{st} (L), 2^{nd} (L)⟩⟩$
63	7 62	eqtrd	$⊢ φ \to Y = ⟨⟨1^{st} (K), 2^{nd} (K)⟩, ⟨1^{st} (L), 2^{nd} (L)⟩⟩$
64	5 55 57 63	fuco111	$⊢ φ \to 1^{st} (O (Y)) = 1^{st} (K) \circ 1^{st} (L)$
65	64	fveq1d	$⊢ φ \to 1^{st} (O (Y)) (x) = (1^{st} (K) \circ 1^{st} (L)) (x)$
66	65	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (Y)) (x) = (1^{st} (K) \circ 1^{st} (L)) (x)$
67	14 48 55	funcf1	$⊢ φ \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
68	67	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
69	68 51	fvco3d	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (K) \circ 1^{st} (L)) (x) = 1^{st} (K) (1^{st} (L) (x))$
70	66 69	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (Y)) (x) = 1^{st} (K) (1^{st} (L) (x))$
71	53 70	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))⟩$
72	27	natrcl	$⊢ V \in (L (C Nat D) N) \to (L \in (C Func D) \land N \in (C Func D))$
73	4 72	syl	$⊢ φ \to (L \in (C Func D) \land N \in (C Func D))$
74	73	simprd	$⊢ φ \to N \in (C Func D)$
75	74	func1st2nd	$⊢ φ \to 1^{st} (N) (C Func D) 2^{nd} (N)$
76	32	natrcl	$⊢ U \in (K (D Nat E) M) \to (K \in (D Func E) \land M \in (D Func E))$
77	3 76	syl	$⊢ φ \to (K \in (D Func E) \land M \in (D Func E))$
78	77	simprd	$⊢ φ \to M \in (D Func E)$
79	78	func1st2nd	$⊢ φ \to 1^{st} (M) (D Func E) 2^{nd} (M)$
80		1st2nd	$⊢ (Rel (D Func E) \land M \in (D Func E)) \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
81	37 78 80	sylancr	$⊢ φ \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
82		1st2nd	$⊢ (Rel (C Func D) \land N \in (C Func D)) \to N = ⟨1^{st} (N), 2^{nd} (N)⟩$
83	40 74 82	sylancr	$⊢ φ \to N = ⟨1^{st} (N), 2^{nd} (N)⟩$
84	81 83	opeq12d	$⊢ φ \to ⟨M, N⟩ = ⟨⟨1^{st} (M), 2^{nd} (M)⟩, ⟨1^{st} (N), 2^{nd} (N)⟩⟩$
85	8 84	eqtrd	$⊢ φ \to Z = ⟨⟨1^{st} (M), 2^{nd} (M)⟩, ⟨1^{st} (N), 2^{nd} (N)⟩⟩$
86	5 75 79 85	fuco111	$⊢ φ \to 1^{st} (O (Z)) = 1^{st} (M) \circ 1^{st} (N)$
87	86	fveq1d	$⊢ φ \to 1^{st} (O (Z)) (x) = (1^{st} (M) \circ 1^{st} (N)) (x)$
88	87	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (Z)) (x) = (1^{st} (M) \circ 1^{st} (N)) (x)$
89	14 48 75	funcf1	$⊢ φ \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
90	89	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
91	90 51	fvco3d	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (M) \circ 1^{st} (N)) (x) = 1^{st} (M) (1^{st} (N) (x))$
92	88 91	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (O (Z)) (x) = 1^{st} (M) (1^{st} (N) (x))$
93	71 92	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))$
94	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)))$
95	23 94	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)))$
96		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$
97	95 96	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))$
98	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)))$
99	18 98	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)))$
100		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$
101	99 100	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))$
102	93 97 101	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)))$
103	102	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))))$
104	26 103	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