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	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 ( 𝐷 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	fucocolem4	⊢ ( 𝜑 → ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐴 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( 𝑉 ‘ 𝑥 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem fucocolem4

Proof