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

Metamath Proof Explorer

Theorem cofu1st2nd

Description: Rewrite the functor composition with separated functor parts. (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Hypotheses cofu1st2nd.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
cofu1st2nd.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
Assertion cofu1st2nd ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = ( ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 cofu1st2nd.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2 cofu1st2nd.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
3 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
4 1st2nd ⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
5 3 2 4 sylancr ⊢ ( 𝜑 → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
6 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
7 1st2nd ⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
8 6 1 7 sylancr ⊢ ( 𝜑 → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
9 5 8 oveq12d ⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = ( ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )