cofu1a

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

Step	Hyp	Ref	Expression
1		cofu1a.b	$⊢ B = {Base}_{C}$
2		cofu1a.f	$⊢ φ \to F (C Func D) G$
3		cofu1a.k	$⊢ φ \to K (D Func E) L$
4		cofu1a.m	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ = ⟨M, N⟩$
5		cofu1a.x	$⊢ φ \to X \in B$
6		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
7	2 6	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
8		df-br	$⊢ K (D Func E) L \leftrightarrow ⟨K, L⟩ \in (D Func E)$
9	3 8	sylib	$⊢ φ \to ⟨K, L⟩ \in (D Func E)$
10	1 7 9 5	cofu1	$⊢ φ \to 1^{st} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) (X) = 1^{st} (⟨K, L⟩) (1^{st} (⟨F, G⟩) (X))$
11	4	fveq2d	$⊢ φ \to 1^{st} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) = 1^{st} (⟨M, N⟩)$
12	7 9	cofucl	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ \in (C Func E)$
13	4 12	eqeltrrd	$⊢ φ \to ⟨M, N⟩ \in (C Func E)$
14		df-br	$⊢ M (C Func E) N \leftrightarrow ⟨M, N⟩ \in (C Func E)$
15	13 14	sylibr	$⊢ φ \to M (C Func E) N$
16	15	func1st	$⊢ φ \to 1^{st} (⟨M, N⟩) = M$
17	11 16	eqtrd	$⊢ φ \to 1^{st} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) = M$
18	17	fveq1d	$⊢ φ \to 1^{st} (⟨K, L⟩ \circ_{func} ⟨F, G⟩) (X) = M (X)$
19	3	func1st	$⊢ φ \to 1^{st} (⟨K, L⟩) = K$
20	2	func1st	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
21	20	fveq1d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) = F (X)$
22	19 21	fveq12d	$⊢ φ \to 1^{st} (⟨K, L⟩) (1^{st} (⟨F, G⟩) (X)) = K (F (X))$
23	10 18 22	3eqtr3rd	$⊢ φ \to K (F (X)) = M (X)$

Metamath Proof Explorer