Theorem fuco111x

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

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

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	1 2 3 4	fuco111	⊢ ( 𝜑 → ( 1st ‘ ( 𝑂 ‘ 𝑈 ) ) = ( 𝐾 ∘ 𝐹 ) )
7	6	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑂 ‘ 𝑈 ) ) ‘ 𝑋 ) = ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10	8 9 2	funcf1	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
11	10 5	fvco3d	⊢ ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑋 ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) )
12	7 11	eqtrd	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑂 ‘ 𝑈 ) ) ‘ 𝑋 ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) )