Theorem fuco112x

Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
	fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
	fuco111x.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
	fuco112x.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
Assertion	fuco112x	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ ( 𝑂 ‘ 𝑈 ) ) 𝑌 ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∘ ( 𝑋 𝐺 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3		fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
4		fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
5		fuco111x.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
6		fuco112x.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
7		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8	1 2 3 4 7	fuco112	⊢ ( 𝜑 → ( 2nd ‘ ( 𝑂 ‘ 𝑈 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
10	9	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
13	10 12	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) )
14	9 11	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑌 ) )
15	13 14	coeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∘ ( 𝑋 𝐺 𝑌 ) ) )
16		ovexd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∈ V )
17		ovexd	⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) ∈ V )
18	16 17	coexd	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∘ ( 𝑋 𝐺 𝑌 ) ) ∈ V )
19	8 15 5 6 18	ovmpod	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ ( 𝑂 ‘ 𝑈 ) ) 𝑌 ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ∘ ( 𝑋 𝐺 𝑌 ) ) )