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		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
28		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
29	28	natrcl	⊢ ( 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
30	2 29	syl	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
31	30	simpld	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
32		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
33	27 31 32	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
34		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
35		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
36	35	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
37	1 36	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
38	37	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
39		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐹 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
40	34 38 39	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
41		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐹 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
42	34 38 41	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
43		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
44	27 31 43	sylancr	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ )
45	42 44	opeq12d	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ⟨ ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ , ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ⟩ )
46	6 45	eqtrd	⊢ ( 𝜑 → 𝑋 = ⟨ ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ , ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ⟩ )
47	5 33 40 46	fuco111	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) = ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) )
48	47	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) ‘ 𝑥 ) = ( ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) ‘ 𝑥 ) = ( ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) )
50		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
51	14 50 33	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
53		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
54	52 53	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
55	49 54	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
56	30	simprd	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝐷 ) )
57		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
58	27 56 57	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
59	37	simprd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
60		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
61	34 59 60	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
62		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
63	34 59 62	sylancr	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
64		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐿 = ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ )
65	27 56 64	sylancr	⊢ ( 𝜑 → 𝐿 = ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ )
66	63 65	opeq12d	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ = ⟨ ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ , ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ⟩ )
67	7 66	eqtrd	⊢ ( 𝜑 → 𝑌 = ⟨ ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ , ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ⟩ )
68	5 58 61 67	fuco111	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) = ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐿 ) ) )
69	68	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ‘ 𝑥 ) = ( ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐿 ) ) ‘ 𝑥 ) )
70	69	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ‘ 𝑥 ) = ( ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐿 ) ) ‘ 𝑥 ) )
71	14 50 58	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
72	71	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
73	72 53	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐿 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) )
74	70 73	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) )
75	55 74	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ⟩ )
76	28	natrcl	⊢ ( 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
77	4 76	syl	⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
78	77	simprd	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐶 Func 𝐷 ) )
79		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
80	27 78 79	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
81	35	natrcl	⊢ ( 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) )
82	3 81	syl	⊢ ( 𝜑 → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) )
83	82	simprd	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐷 Func 𝐸 ) )
84		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝑀 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑀 ) )
85	34 83 84	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑀 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑀 ) )
86		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) → 𝑀 = ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ )
87	34 83 86	sylancr	⊢ ( 𝜑 → 𝑀 = ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ )
88		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑁 = ⟨ ( 1^st ‘ 𝑁 ) , ( 2^nd ‘ 𝑁 ) ⟩ )
89	27 78 88	sylancr	⊢ ( 𝜑 → 𝑁 = ⟨ ( 1^st ‘ 𝑁 ) , ( 2^nd ‘ 𝑁 ) ⟩ )
90	87 89	opeq12d	⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ = ⟨ ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ , ⟨ ( 1^st ‘ 𝑁 ) , ( 2^nd ‘ 𝑁 ) ⟩ ⟩ )
91	8 90	eqtrd	⊢ ( 𝜑 → 𝑍 = ⟨ ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ , ⟨ ( 1^st ‘ 𝑁 ) , ( 2^nd ‘ 𝑁 ) ⟩ ⟩ )
92	5 80 85 91	fuco111	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) = ( ( 1^st ‘ 𝑀 ) ∘ ( 1^st ‘ 𝑁 ) ) )
93	92	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) ‘ 𝑥 ) = ( ( ( 1^st ‘ 𝑀 ) ∘ ( 1^st ‘ 𝑁 ) ) ‘ 𝑥 ) )
94	93	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) ‘ 𝑥 ) = ( ( ( 1^st ‘ 𝑀 ) ∘ ( 1^st ‘ 𝑁 ) ) ‘ 𝑥 ) )
95	14 50 80	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
96	95	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝑁 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
97	96 53	fvco3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ 𝑀 ) ∘ ( 1^st ‘ 𝑁 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
98	94 97	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) )
99	75 98	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 𝑂 ‘ 𝑍 ) ) ‘ 𝑥 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) )
100	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 ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( 𝑉 ‘ 𝑥 ) ) ) ) )
101	23 100	eqtrd	⊢ ( 𝜑 → ( ( 𝑌 𝑃 𝑍 ) ‘ 𝐵 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( 𝑉 ‘ 𝑥 ) ) ) ) )
102		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( 𝑉 ‘ 𝑥 ) ) ) ∈ V )
103	101 102	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑁 ) ‘ 𝑥 ) ) ‘ ( 𝑉 ‘ 𝑥 ) ) ) )
104	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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) )
105	18 104	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐴 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) )
106		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ∈ V )
107	105 106	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑅 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) )
108	99 103 107	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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) )
109	108	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 ‘ 𝐿 ) ‘ 𝑥 ) ) ‘ ( 𝑆 ‘ 𝑥 ) ) ) ) ) )
110	26 109	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