Theorem cofid1

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

	Ref	Expression
Hypotheses	cofid1a.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
	cofid1a.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	cofid1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cofid1.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	cofid1.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
	cofid1.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
Assertion	cofid1	⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		cofid1a.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
2		cofid1a.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		cofid1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		cofid1.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5		cofid1.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
6		cofid1.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
7	5	func1st	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
8	4	func1st	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
9	8	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
10	7 9	fveq12d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ‘ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) )
11		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
12	4 11	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
13		df-br	⊢ ( 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐸 Func 𝐷 ) )
14	5 13	sylib	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐸 Func 𝐷 ) )
15	1 2 3 12 14 6	cofid1a	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ‘ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ) = 𝑋 )
16	10 15	eqtr3d	⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )