Theorem cofu1a

Description: Value of the object part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	cofu1a.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	cofu1a.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	cofu1a.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
	cofu1a.m	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝑀 , 𝑁 ⟩ )
	cofu1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	cofu1a	⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝑀 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		cofu1a.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		cofu1a.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3		cofu1a.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
4		cofu1a.m	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝑀 , 𝑁 ⟩ )
5		cofu1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		df-br	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
7	2 6	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
8		df-br	⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
9	3 8	sylib	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
10	1 7 9 5	cofu1	⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) ‘ 𝑋 ) = ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ‘ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ) )
11	4	fveq2d	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
12	7 9	cofucl	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ∈ ( 𝐶 Func 𝐸 ) )
13	4 12	eqeltrrd	⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
14		df-br	⊢ ( 𝑀 ( 𝐶 Func 𝐸 ) 𝑁 ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
15	13 14	sylibr	⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐸 ) 𝑁 )
16	15	func1st	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
17	11 16	eqtrd	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = 𝑀 )
18	17	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) ‘ 𝑋 ) = ( 𝑀 ‘ 𝑋 ) )
19	3	func1st	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
20	2	func1st	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
21	20	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
22	19 21	fveq12d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ‘ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) )
23	10 18 22	3eqtr3rd	⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝑀 ‘ 𝑋 ) )