cofid1

Description: Express the object part of ( G o.func F ) = I explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

Step	Hyp	Ref	Expression
1		cofid1a.i	$⊢ I = {id}_{func} (D)$
2		cofid1a.b	$⊢ B = {Base}_{D}$
3		cofid1a.x	$⊢ φ \to X \in B$
4		cofid1.f	$⊢ φ \to F (D Func E) G$
5		cofid1.k	$⊢ φ \to K (E Func D) L$
6		cofid1.o	$⊢ φ \to ⟨K, L⟩ \circ_{func} ⟨F, G⟩ = I$
7	5	func1st	$⊢ φ \to 1^{st} (⟨K, L⟩) = K$
8	4	func1st	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
9	8	fveq1d	$⊢ φ \to 1^{st} (⟨F, G⟩) (X) = F (X)$
10	7 9	fveq12d	$⊢ φ \to 1^{st} (⟨K, L⟩) (1^{st} (⟨F, G⟩) (X)) = K (F (X))$
11		df-br	$⊢ F (D Func E) G \leftrightarrow ⟨F, G⟩ \in (D Func E)$
12	4 11	sylib	$⊢ φ \to ⟨F, G⟩ \in (D Func E)$
13		df-br	$⊢ K (E Func D) L \leftrightarrow ⟨K, L⟩ \in (E Func D)$
14	5 13	sylib	$⊢ φ \to ⟨K, L⟩ \in (E Func D)$
15	1 2 3 12 14 6	cofid1a	$⊢ φ \to 1^{st} (⟨K, L⟩) (1^{st} (⟨F, G⟩) (X)) = X$
16	10 15	eqtr3d	$⊢ φ \to K (F (X)) = X$

Metamath Proof Explorer