Theorem fuco112

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	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
	fuco11a.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	fuco112	⊢ ( 𝜑 → ( 2nd ‘ ( 𝑂 ‘ 𝑈 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3		fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
4		fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
5		fuco11a.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
6	1 2 3 4 5	fuco11a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑈 ) = ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )
7	6	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ ( 𝑂 ‘ 𝑈 ) ) = ( 2nd ‘ ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ ) )
8		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
9	8	brrelex1i	⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 → 𝐾 ∈ V )
10	3 9	syl	⊢ ( 𝜑 → 𝐾 ∈ V )
11		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
12	11	brrelex1i	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → 𝐹 ∈ V )
13	2 12	syl	⊢ ( 𝜑 → 𝐹 ∈ V )
14	10 13	coexd	⊢ ( 𝜑 → ( 𝐾 ∘ 𝐹 ) ∈ V )
15	5	fvexi	⊢ 𝐵 ∈ V
16	15 15	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ∈ V
17		op2ndg	⊢ ( ( ( 𝐾 ∘ 𝐹 ) ∈ V ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ∈ V ) → ( 2nd ‘ ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) )
18	14 16 17	sylancl	⊢ ( 𝜑 → ( 2nd ‘ ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) )
19	7 18	eqtrd	⊢ ( 𝜑 → ( 2nd ‘ ( 𝑂 ‘ 𝑈 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) )