Theorem fucocolem4 48923

Description: Lemma for fucoco 48924. The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-Oct-2025.)

Hypotheses

Ref	Expression
fucoco.r	⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))
fucoco.s	⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))
fucoco.u	⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))
fucoco.v	⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))
fucoco.o	⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)
fucoco.x	⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)
fucoco.y	⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)
fucoco.z	⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)
fucoco.a	⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)
fucoco.b	⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)
fucoco.q	⊢ 𝑄 = (𝐶 FuncCat 𝐸)
fucoco.oq	⊢ ∙ = (comp‘𝑄)

Assertion

Ref

Expression

fucocolem4

⊢ (𝜑 → (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))))))

Distinct variable groups:   𝑥,𝐶   𝑥,𝐷   𝑥,𝐸   𝑥,𝐹   𝑥,𝐺   𝑥,𝐾   𝑥,𝐿   𝑥,𝑀   𝑥,𝑁   𝑥,𝑅   𝑥,𝑆   𝑥,𝑈   𝑥,𝑉   𝑥,𝑋   𝑥,𝑍   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵   𝑥,𝑂   𝑥,𝑃   𝑥,𝑌

Allowed substitution hints:   𝑄(𝑥)   ∙ (𝑥)

Proof of Theorem fucocolem4

Step	Hyp	Ref	Expression
1		fucoco.q	. . 3 ⊢ 𝑄 = (𝐶 FuncCat 𝐸)
2		eqid 2737	. . 3 ⊢ (𝐶 Nat 𝐸) = (𝐶 Nat 𝐸)
3		eqid 2737	. . 3 ⊢ (Base‘𝐶) = (Base‘𝐶)
4		eqid 2737	. . 3 ⊢ (comp‘𝐸) = (comp‘𝐸)
5		fucoco.oq	. . 3 ⊢ ∙ = (comp‘𝑄)
6		fucoco.a	. . . . . 6 ⊢ (𝜑 → 𝐴 = ⟨𝑅, 𝑆⟩)
7	6	fveq2d 6918	. . . . 5 ⊢ (𝜑 → ((𝑋𝑃𝑌)‘𝐴) = ((𝑋𝑃𝑌)‘⟨𝑅, 𝑆⟩))
8		df-ov 7441	. . . . 5 ⊢ (𝑅(𝑋𝑃𝑌)𝑆) = ((𝑋𝑃𝑌)‘⟨𝑅, 𝑆⟩)
9	7, 8	eqtr4di 2795	. . . 4 ⊢ (𝜑 → ((𝑋𝑃𝑌)‘𝐴) = (𝑅(𝑋𝑃𝑌)𝑆))
10		fucoco.o	. . . . 5 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)
11		fucoco.s	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿))
12		fucoco.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾))
13		fucoco.x	. . . . 5 ⊢ (𝜑 → 𝑋 = ⟨𝐹, 𝐺⟩)
14		fucoco.y	. . . . 5 ⊢ (𝜑 → 𝑌 = ⟨𝐾, 𝐿⟩)
15	10, 11, 12, 13, 14	fuco22nat 48913	. . . 4 ⊢ (𝜑 → (𝑅(𝑋𝑃𝑌)𝑆) ∈ ((𝑂‘𝑋)(𝐶 Nat 𝐸)(𝑂‘𝑌)))
16	9, 15	eqeltrd 2841	. . 3 ⊢ (𝜑 → ((𝑋𝑃𝑌)‘𝐴) ∈ ((𝑂‘𝑋)(𝐶 Nat 𝐸)(𝑂‘𝑌)))
17		fucoco.b	. . . . . 6 ⊢ (𝜑 → 𝐵 = ⟨𝑈, 𝑉⟩)
18	17	fveq2d 6918	. . . . 5 ⊢ (𝜑 → ((𝑌𝑃𝑍)‘𝐵) = ((𝑌𝑃𝑍)‘⟨𝑈, 𝑉⟩))
19		df-ov 7441	. . . . 5 ⊢ (𝑈(𝑌𝑃𝑍)𝑉) = ((𝑌𝑃𝑍)‘⟨𝑈, 𝑉⟩)
20	18, 19	eqtr4di 2795	. . . 4 ⊢ (𝜑 → ((𝑌𝑃𝑍)‘𝐵) = (𝑈(𝑌𝑃𝑍)𝑉))
21		fucoco.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁))
22		fucoco.u	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀))
23		fucoco.z	. . . . 5 ⊢ (𝜑 → 𝑍 = ⟨𝑀, 𝑁⟩)
24	10, 21, 22, 14, 23	fuco22nat 48913	. . . 4 ⊢ (𝜑 → (𝑈(𝑌𝑃𝑍)𝑉) ∈ ((𝑂‘𝑌)(𝐶 Nat 𝐸)(𝑂‘𝑍)))
25	20, 24	eqeltrd 2841	. . 3 ⊢ (𝜑 → ((𝑌𝑃𝑍)‘𝐵) ∈ ((𝑂‘𝑌)(𝐶 Nat 𝐸)(𝑂‘𝑍)))
26	1, 2, 3, 4, 5, 16, 25	fucco 18028	. 2 ⊢ (𝜑 → (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ ((((𝑌𝑃𝑍)‘𝐵)‘𝑥)(⟨((1st ‘(𝑂‘𝑋))‘𝑥), ((1st ‘(𝑂‘𝑌))‘𝑥)⟩(comp‘𝐸)((1st ‘(𝑂‘𝑍))‘𝑥))(((𝑋𝑃𝑌)‘𝐴)‘𝑥))))
27		relfunc 17922	. . . . . . . . . . 11 ⊢ Rel (𝐶 Func 𝐷)
28		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
29	28	natrcl 18014	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (𝐺(𝐶 Nat 𝐷)𝐿) → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝐿 ∈ (𝐶 Func 𝐷)))
30	11, 29	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝐿 ∈ (𝐶 Func 𝐷)))
31	30	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))
32		1st2ndbr 8075	. . . . . . . . . . 11 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺))
33	27, 31, 32	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺))
34		relfunc 17922	. . . . . . . . . . 11 ⊢ Rel (𝐷 Func 𝐸)
35		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝐷 Nat 𝐸) = (𝐷 Nat 𝐸)
36	35	natrcl 18014	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ (𝐹(𝐷 Nat 𝐸)𝐾) → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝐾 ∈ (𝐷 Func 𝐸)))
37	12, 36	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ (𝐷 Func 𝐸) ∧ 𝐾 ∈ (𝐷 Func 𝐸)))
38	37	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (𝐷 Func 𝐸))
39		1st2ndbr 8075	. . . . . . . . . . 11 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝐹 ∈ (𝐷 Func 𝐸)) → (1st ‘𝐹)(𝐷 Func 𝐸)(2nd ‘𝐹))
40	34, 38, 39	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐹)(𝐷 Func 𝐸)(2nd ‘𝐹))
41		1st2nd 8072	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝐹 ∈ (𝐷 Func 𝐸)) → 𝐹 = ⟨(1st ‘𝐹), (2nd ‘𝐹)⟩)
42	34, 38, 41	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 = ⟨(1st ‘𝐹), (2nd ‘𝐹)⟩)
43		1st2nd 8072	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → 𝐺 = ⟨(1st ‘𝐺), (2nd ‘𝐺)⟩)
44	27, 31, 43	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = ⟨(1st ‘𝐺), (2nd ‘𝐺)⟩)
45	42, 44	opeq12d 4889	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ = ⟨⟨(1st ‘𝐹), (2nd ‘𝐹)⟩, ⟨(1st ‘𝐺), (2nd ‘𝐺)⟩⟩)
46	13, 45	eqtrd 2777	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ⟨⟨(1st ‘𝐹), (2nd ‘𝐹)⟩, ⟨(1st ‘𝐺), (2nd ‘𝐺)⟩⟩)
47	10, 33, 40, 46	fuco111 48899	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘(𝑂‘𝑋)) = ((1st ‘𝐹) ∘ (1st ‘𝐺)))
48	47	fveq1d 6916	. . . . . . . 8 ⊢ (𝜑 → ((1st ‘(𝑂‘𝑋))‘𝑥) = (((1st ‘𝐹) ∘ (1st ‘𝐺))‘𝑥))
49	48	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝑂‘𝑋))‘𝑥) = (((1st ‘𝐹) ∘ (1st ‘𝐺))‘𝑥))
50		eqid 2737	. . . . . . . . . 10 ⊢ (Base‘𝐷) = (Base‘𝐷)
51	3, 50, 33	funcf1 17926	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝐺):(Base‘𝐶)⟶(Base‘𝐷))
52	51	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺):(Base‘𝐶)⟶(Base‘𝐷))
53		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
54	52, 53	fvco3d 7016	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((1st ‘𝐹) ∘ (1st ‘𝐺))‘𝑥) = ((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)))
55	49, 54	eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝑂‘𝑋))‘𝑥) = ((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)))
56	30	simprd 495	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ (𝐶 Func 𝐷))
57		1st2ndbr 8075	. . . . . . . . . . 11 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐿 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐿)(𝐶 Func 𝐷)(2nd ‘𝐿))
58	27, 56, 57	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐿)(𝐶 Func 𝐷)(2nd ‘𝐿))
59	37	simprd 495	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))
60		1st2ndbr 8075	. . . . . . . . . . 11 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝐾 ∈ (𝐷 Func 𝐸)) → (1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾))
61	34, 59, 60	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾))
62		1st2nd 8072	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝐾 ∈ (𝐷 Func 𝐸)) → 𝐾 = ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩)
63	34, 59, 62	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 = ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩)
64		1st2nd 8072	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐿 ∈ (𝐶 Func 𝐷)) → 𝐿 = ⟨(1st ‘𝐿), (2nd ‘𝐿)⟩)
65	27, 56, 64	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 = ⟨(1st ‘𝐿), (2nd ‘𝐿)⟩)
66	63, 65	opeq12d 4889	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨𝐾, 𝐿⟩ = ⟨⟨(1st ‘𝐾), (2nd ‘𝐾)⟩, ⟨(1st ‘𝐿), (2nd ‘𝐿)⟩⟩)
67	14, 66	eqtrd 2777	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 = ⟨⟨(1st ‘𝐾), (2nd ‘𝐾)⟩, ⟨(1st ‘𝐿), (2nd ‘𝐿)⟩⟩)
68	10, 58, 61, 67	fuco111 48899	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘(𝑂‘𝑌)) = ((1st ‘𝐾) ∘ (1st ‘𝐿)))
69	68	fveq1d 6916	. . . . . . . 8 ⊢ (𝜑 → ((1st ‘(𝑂‘𝑌))‘𝑥) = (((1st ‘𝐾) ∘ (1st ‘𝐿))‘𝑥))
70	69	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝑂‘𝑌))‘𝑥) = (((1st ‘𝐾) ∘ (1st ‘𝐿))‘𝑥))
71	3, 50, 58	funcf1 17926	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝐿):(Base‘𝐶)⟶(Base‘𝐷))
72	71	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐿):(Base‘𝐶)⟶(Base‘𝐷))
73	72, 53	fvco3d 7016	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((1st ‘𝐾) ∘ (1st ‘𝐿))‘𝑥) = ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))
74	70, 73	eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝑂‘𝑌))‘𝑥) = ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))
75	55, 74	opeq12d 4889	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ⟨((1st ‘(𝑂‘𝑋))‘𝑥), ((1st ‘(𝑂‘𝑌))‘𝑥)⟩ = ⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩)
76	28	natrcl 18014	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ (𝐿(𝐶 Nat 𝐷)𝑁) → (𝐿 ∈ (𝐶 Func 𝐷) ∧ 𝑁 ∈ (𝐶 Func 𝐷)))
77	21, 76	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ∈ (𝐶 Func 𝐷) ∧ 𝑁 ∈ (𝐶 Func 𝐷)))
78	77	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (𝐶 Func 𝐷))
79		1st2ndbr 8075	. . . . . . . . . 10 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑁 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑁)(𝐶 Func 𝐷)(2nd ‘𝑁))
80	27, 78, 79	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝑁)(𝐶 Func 𝐷)(2nd ‘𝑁))
81	35	natrcl 18014	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (𝐾(𝐷 Nat 𝐸)𝑀) → (𝐾 ∈ (𝐷 Func 𝐸) ∧ 𝑀 ∈ (𝐷 Func 𝐸)))
82	22, 81	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 ∈ (𝐷 Func 𝐸) ∧ 𝑀 ∈ (𝐷 Func 𝐸)))
83	82	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (𝐷 Func 𝐸))
84		1st2ndbr 8075	. . . . . . . . . 10 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝑀 ∈ (𝐷 Func 𝐸)) → (1st ‘𝑀)(𝐷 Func 𝐸)(2nd ‘𝑀))
85	34, 83, 84	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝑀)(𝐷 Func 𝐸)(2nd ‘𝑀))
86		1st2nd 8072	. . . . . . . . . . . 12 ⊢ ((Rel (𝐷 Func 𝐸) ∧ 𝑀 ∈ (𝐷 Func 𝐸)) → 𝑀 = ⟨(1st ‘𝑀), (2nd ‘𝑀)⟩)
87	34, 83, 86	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 = ⟨(1st ‘𝑀), (2nd ‘𝑀)⟩)
88		1st2nd 8072	. . . . . . . . . . . 12 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑁 ∈ (𝐶 Func 𝐷)) → 𝑁 = ⟨(1st ‘𝑁), (2nd ‘𝑁)⟩)
89	27, 78, 88	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = ⟨(1st ‘𝑁), (2nd ‘𝑁)⟩)
90	87, 89	opeq12d 4889	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝑀, 𝑁⟩ = ⟨⟨(1st ‘𝑀), (2nd ‘𝑀)⟩, ⟨(1st ‘𝑁), (2nd ‘𝑁)⟩⟩)
91	23, 90	eqtrd 2777	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 = ⟨⟨(1st ‘𝑀), (2nd ‘𝑀)⟩, ⟨(1st ‘𝑁), (2nd ‘𝑁)⟩⟩)
92	10, 80, 85, 91	fuco111 48899	. . . . . . . 8 ⊢ (𝜑 → (1st ‘(𝑂‘𝑍)) = ((1st ‘𝑀) ∘ (1st ‘𝑁)))
93	92	fveq1d 6916	. . . . . . 7 ⊢ (𝜑 → ((1st ‘(𝑂‘𝑍))‘𝑥) = (((1st ‘𝑀) ∘ (1st ‘𝑁))‘𝑥))
94	93	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝑂‘𝑍))‘𝑥) = (((1st ‘𝑀) ∘ (1st ‘𝑁))‘𝑥))
95	3, 50, 80	funcf1 17926	. . . . . . . 8 ⊢ (𝜑 → (1st ‘𝑁):(Base‘𝐶)⟶(Base‘𝐷))
96	95	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝑁):(Base‘𝐶)⟶(Base‘𝐷))
97	96, 53	fvco3d 7016	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((1st ‘𝑀) ∘ (1st ‘𝑁))‘𝑥) = ((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))
98	94, 97	eqtrd 2777	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝑂‘𝑍))‘𝑥) = ((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))
99	75, 98	oveq12d 7456	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (⟨((1st ‘(𝑂‘𝑋))‘𝑥), ((1st ‘(𝑂‘𝑌))‘𝑥)⟩(comp‘𝐸)((1st ‘(𝑂‘𝑍))‘𝑥)) = (⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥))))
100	10, 14, 23, 21, 22	fuco22a 48917	. . . . . 6 ⊢ (𝜑 → (𝑈(𝑌𝑃𝑍)𝑉) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))))
101	20, 100	eqtrd 2777	. . . . 5 ⊢ (𝜑 → ((𝑌𝑃𝑍)‘𝐵) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))))
102		ovexd 7473	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥))) ∈ V)
103	101, 102	fvmpt2d 7036	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((𝑌𝑃𝑍)‘𝐵)‘𝑥) = ((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥))))
104	10, 13, 14, 11, 12	fuco22a 48917	. . . . . 6 ⊢ (𝜑 → (𝑅(𝑋𝑃𝑌)𝑆) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥)))))
105	9, 104	eqtrd 2777	. . . . 5 ⊢ (𝜑 → ((𝑋𝑃𝑌)‘𝐴) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥)))))
106		ovexd 7473	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))) ∈ V)
107	105, 106	fvmpt2d 7036	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((𝑋𝑃𝑌)‘𝐴)‘𝑥) = ((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))))
108	99, 103, 107	oveq123d 7459	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((𝑌𝑃𝑍)‘𝐵)‘𝑥)(⟨((1st ‘(𝑂‘𝑋))‘𝑥), ((1st ‘(𝑂‘𝑌))‘𝑥)⟩(comp‘𝐸)((1st ‘(𝑂‘𝑍))‘𝑥))(((𝑋𝑃𝑌)‘𝐴)‘𝑥)) = (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥)))))
109	108	mpteq2dva 5251	. 2 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ ((((𝑌𝑃𝑍)‘𝐵)‘𝑥)(⟨((1st ‘(𝑂‘𝑋))‘𝑥), ((1st ‘(𝑂‘𝑌))‘𝑥)⟩(comp‘𝐸)((1st ‘(𝑂‘𝑍))‘𝑥))(((𝑋𝑃𝑌)‘𝐴)‘𝑥))) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))))))
110	26, 109	eqtrd 2777	1 ⊢ (𝜑 → (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)) = (𝑥 ∈ (Base‘𝐶) ↦ (((𝑈‘((1st ‘𝑁)‘𝑥))(⟨((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝑁)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((((1st ‘𝐿)‘𝑥)(2nd ‘𝐾)((1st ‘𝑁)‘𝑥))‘(𝑉‘𝑥)))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝑀)‘((1st ‘𝑁)‘𝑥)))((𝑅‘((1st ‘𝐿)‘𝑥))(⟨((1st ‘𝐹)‘((1st ‘𝐺)‘𝑥)), ((1st ‘𝐹)‘((1st ‘𝐿)‘𝑥))⟩(comp‘𝐸)((1st ‘𝐾)‘((1st ‘𝐿)‘𝑥)))((((1st ‘𝐺)‘𝑥)(2nd ‘𝐹)((1st ‘𝐿)‘𝑥))‘(𝑆‘𝑥))))))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3481  ⟨cop 4640   class class class wbr 5151   ↦ cmpt 5234   ∘ ccom 5697  Rel wrel 5698  ⟶wf 6565  ‘cfv 6569  (class class class)co 7438  1^st c1st 8020  2^nd c2nd 8021  Basecbs 17254  compcco 17319   Func cfunc 17914   Nat cnat 18005   FuncCat cfuc 18006   ∘_F cfuco 48885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5288  ax-sep 5305  ax-nul 5315  ax-pow 5374  ax-pr 5441  ax-un 7761  ax-cnex 11218  ax-resscn 11219  ax-1cn 11220  ax-icn 11221  ax-addcl 11222  ax-addrcl 11223  ax-mulcl 11224  ax-mulrcl 11225  ax-mulcom 11226  ax-addass 11227  ax-mulass 11228  ax-distr 11229  ax-i2m1 11230  ax-1ne0 11231  ax-1rid 11232  ax-rnegex 11233  ax-rrecex 11234  ax-cnre 11235  ax-pre-lttri 11236  ax-pre-lttrn 11237  ax-pre-ltadd 11238  ax-pre-mulgt0 11239

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3483  df-sbc 3795  df-csb 3912  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-pss 3986  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-tp 4639  df-op 4641  df-uni 4916  df-iun 5001  df-br 5152  df-opab 5214  df-mpt 5235  df-tr 5269  df-id 5587  df-eprel 5593  df-po 5601  df-so 5602  df-fr 5645  df-we 5647  df-xp 5699  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-res 5705  df-ima 5706  df-pred 6329  df-ord 6395  df-on 6396  df-lim 6397  df-suc 6398  df-iota 6522  df-fun 6571  df-fn 6572  df-f 6573  df-f1 6574  df-fo 6575  df-f1o 6576  df-fv 6577  df-riota 7395  df-ov 7441  df-oprab 7442  df-mpo 7443  df-om 7895  df-1st 8022  df-2nd 8023  df-frecs 8314  df-wrecs 8345  df-recs 8419  df-rdg 8458  df-1o 8514  df-er 8753  df-map 8876  df-ixp 8946  df-en 8994  df-dom 8995  df-sdom 8996  df-fin 8997  df-pnf 11304  df-mnf 11305  df-xr 11306  df-ltxr 11307  df-le 11308  df-sub 11501  df-neg 11502  df-nn 12274  df-2 12336  df-3 12337  df-4 12338  df-5 12339  df-6 12340  df-7 12341  df-8 12342  df-9 12343  df-n0 12534  df-z 12621  df-dec 12741  df-uz 12886  df-fz 13554  df-struct 17190  df-slot 17225  df-ndx 17237  df-base 17255  df-hom 17331  df-cco 17332  df-cat 17722  df-cid 17723  df-func 17918  df-cofu 17920  df-nat 18007  df-fuc 18008  df-fuco 48886

This theorem is referenced by:  fucoco  48924