Theorem fuco11idx

Description: The identity morphism of the mapped object. (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
	fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
	fuco11id.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fuco11id.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
	fuco11id.1	⊢ 1 = ( Id ‘ 𝐸 )
	fuco11idx.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
Assertion	fuco11idx	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) ‘ 𝑋 ) = ( 1 ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3		fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
4		fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
5		fuco11id.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
6		fuco11id.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
7		fuco11id.1	⊢ 1 = ( Id ‘ 𝐸 )
8		fuco11idx.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
9	1 2 3 4 5 6 7	fuco11id	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) = ( 1 ∘ ( 𝐾 ∘ 𝐹 ) ) )
10		coass	⊢ ( ( 1 ∘ 𝐾 ) ∘ 𝐹 ) = ( 1 ∘ ( 𝐾 ∘ 𝐹 ) )
11	9 10	eqtr4di	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) = ( ( 1 ∘ 𝐾 ) ∘ 𝐹 ) )
12	11	fveq1d	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) ‘ 𝑋 ) = ( ( ( 1 ∘ 𝐾 ) ∘ 𝐹 ) ‘ 𝑋 ) )
13		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
14		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
15	13 14 2	funcf1	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
16	15 8	fvco3d	⊢ ( 𝜑 → ( ( ( 1 ∘ 𝐾 ) ∘ 𝐹 ) ‘ 𝑋 ) = ( ( 1 ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
17		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
18	14 17 3	funcf1	⊢ ( 𝜑 → 𝐾 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
19	15 8	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
20	18 19	fvco3d	⊢ ( 𝜑 → ( ( 1 ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 1 ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
21	12 16 20	3eqtrd	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) ‘ 𝑋 ) = ( 1 ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )