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	2	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
5	4	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6	3	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
7	6	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
8	6	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
9		eqidd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) )
10	5 7 8 9	fucoelvv	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( V × V ) )
11		1st2nd2	⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( V × V ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ )
12	10 11	syl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ )
13		eqidd	⊢ ( 𝜑 → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
14	5 7 8 12 13	fuco1	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) = ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
15	1 14	eqtr3d	⊢ ( 𝜑 → 𝑂 = ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
16	15	oveqd	⊢ ( 𝜑 → ( 𝐺 𝑂 𝐹 ) = ( 𝐺 ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) 𝐹 ) )
17		ovres	⊢ ( ( 𝐺 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 𝐺 ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )
18	3 2 17	syl2anc	⊢ ( 𝜑 → ( 𝐺 ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )
19	16 18	eqtrd	⊢ ( 𝜑 → ( 𝐺 𝑂 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )