Theorem cofid2a

Description: Express the morphism 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	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cofid1a.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
	cofid1a.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐸 Func 𝐷 ) )
	cofid1a.o	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = 𝐼 )
	cofid2a.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	cofid2a.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	cofid2a.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	cofid2a	⊢ ( 𝜑 → ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		cofid1a.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
2		cofid1a.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		cofid1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		cofid1a.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
5		cofid1a.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐸 Func 𝐷 ) )
6		cofid1a.o	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = 𝐼 )
7		cofid2a.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		cofid2a.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
9		cofid2a.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
10	6	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 ∘func 𝐹 ) ) = ( 2nd ‘ 𝐼 ) )
11	10	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ ( 𝐺 ∘func 𝐹 ) ) 𝑌 ) = ( 𝑋 ( 2nd ‘ 𝐼 ) 𝑌 ) )
12	11	fveq1d	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( 𝐺 ∘func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( 𝑋 ( 2nd ‘ 𝐼 ) 𝑌 ) ‘ 𝑅 ) )
13	2 4 5 3 7 8 9	cofu2	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( 𝐺 ∘func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )
14	4	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
15	14	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
16	1 2 15 8 3 7 9	idfu2	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝐼 ) 𝑌 ) ‘ 𝑅 ) = 𝑅 )
17	12 13 16	3eqtr3d	⊢ ( 𝜑 → ( ( ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) = 𝑅 )