This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐹 ) ‘ 𝑋 ) ) = 𝑋 )