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

Metamath Proof Explorer

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