Metamath Proof Explorer

Theorem fuco11b

Description: The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 11-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 fuco11b.o ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) = 𝑂 )
2 fuco11b.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3 fuco11b.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
4 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
5 1st2ndbr ⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
6 4 2 5 sylancr ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
7 6 funcrcl2 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
8 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
9 1st2ndbr ⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
10 8 3 9 sylancr ⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
11 10 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
12 10 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
13 eqidd ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) )
14 7 11 12 13 fucoelvv ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( V × V ) )
15 1st2nd2 ⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( V × V ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ )
16 14 15 syl ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ )
17 eqidd ⊢ ( 𝜑 → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
18 7 11 12 16 17 fuco1 ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) = ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
19 1 18 eqtr3d ⊢ ( 𝜑 → 𝑂 = ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
20 19 oveqd ⊢ ( 𝜑 → ( 𝐺 𝑂 𝐹 ) = ( 𝐺 ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) 𝐹 ) )
21 ovres ⊢ ( ( 𝐺 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 𝐺 ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )
22 3 2 21 syl2anc ⊢ ( 𝜑 → ( 𝐺 ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )
23 20 22 eqtrd ⊢ ( 𝜑 → ( 𝐺 𝑂 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )