fucoisfunc2

Description: Full componentwise characterization of an arbitrary morphism part with the object function of functor composition. See also fucoisfunc .

Its three exact function domains, component types and naturality, and pointwise identity and composition laws are necessary and sufficient. Empty object and hom domains are permitted. For a concrete failure of uniqueness, see fuconuniq and fuconuniqex2 . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fucoisfunc.w	⊢ 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
	fucoisfunc2lem1.o	⊢ 𝑂 = ( ∘_func ↾ 𝑊 )
	fucoisfunc2lem1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	fucoisfunc2lem1.r	⊢ 𝑅 = ( Hom ‘ 𝐶 )
	fucoisfunc2lem1.s	⊢ 𝑆 = ( Hom ‘ 𝐸 )
	fucoisfunc2lem1.v	⊢ ∙ = ( comp ‘ 𝐸 )
	fucoisfunc2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
	fucoisfunc2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoisfunc2.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
	fucoisfunc2.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
	fucoisfunc2.x	⊢ · = ( comp ‘ 𝑇 )
	fucoisfunc2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoisfunc2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	fucoisfunc2.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	fucoisfunc2.k	⊢ 𝐾 = ( Id ‘ 𝐸 )
Assertion	fucoisfunc2	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	⊢ 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
2		fucoisfunc2lem1.o	⊢ 𝑂 = ( ∘_func ↾ 𝑊 )
3		fucoisfunc2lem1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		fucoisfunc2lem1.r	⊢ 𝑅 = ( Hom ‘ 𝐶 )
5		fucoisfunc2lem1.s	⊢ 𝑆 = ( Hom ‘ 𝐸 )
6		fucoisfunc2lem1.v	⊢ ∙ = ( comp ‘ 𝐸 )
7		fucoisfunc2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
8		fucoisfunc2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
9		fucoisfunc2.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
10		fucoisfunc2.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
11		fucoisfunc2.x	⊢ · = ( comp ‘ 𝑇 )
12		fucoisfunc2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13		fucoisfunc2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
14		fucoisfunc2.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
15		fucoisfunc2.k	⊢ 𝐾 = ( Id ‘ 𝐸 )
16		eqid	⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 )
17		eqid	⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	fucoisfunc2lem2	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) ) )

Metamath Proof Explorer

Theorem fucoisfunc2

Proof