Theorem cofid1a

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	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cofid1a.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
	cofid1a.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐸 Func 𝐷 ) )
	cofid1a.o	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = 𝐼 )
Assertion	cofid1a	⊢ ( 𝜑 → ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) = 𝑋 )

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	6	fveq2d	⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) = ( 1st ‘ 𝐼 ) )
8	7	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐼 ) ‘ 𝑋 ) )
9	2 4 5 3	cofu1	⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ∘func 𝐹 ) ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) )
10	4	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
11	10	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
12	1 2 11 3	idfu1	⊢ ( 𝜑 → ( ( 1st ‘ 𝐼 ) ‘ 𝑋 ) = 𝑋 )
13	8 9 12	3eqtr3d	⊢ ( 𝜑 → ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑋 ) ) = 𝑋 )