Metamath Proof Explorer

Theorem 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 ⊢ W = D Func E × C Func D
fucoisfunc2lem1.o ⊢ O = ∘ func ↾ W
fucoisfunc2lem1.b ⊢ B = Base C
fucoisfunc2lem1.r ⊢ R = Hom ⁡ C
fucoisfunc2lem1.s ⊢ S = Hom ⁡ E
fucoisfunc2lem1.v ⊢ ∙ ˙ = comp ⁡ E
fucoisfunc2.t ⊢ T = D FuncCat E × c C FuncCat D
fucoisfunc2.q ⊢ Q = C FuncCat E
fucoisfunc2.h ⊢ H = Hom ⁡ T
fucoisfunc2.i ⊢ I = Id ⁡ T
fucoisfunc2.x ⊢ · ˙ = comp ⁡ T
fucoisfunc2.c ⊢ φ → C ∈ Cat
fucoisfunc2.d ⊢ φ → D ∈ Cat
fucoisfunc2.e ⊢ φ → E ∈ Cat
fucoisfunc2.k ⊢ K = Id ⁡ E
Assertion fucoisfunc2 ⊢ φ → O T Func Q P ↔ P = u ∈ W , v ∈ W ⟼ u P v ∧ ∀ m ∈ W ∀ n ∈ W m P n = b ∈ 1 st ⁡ m D Nat E 1 st ⁡ n , a ∈ 2 nd ⁡ m C Nat D 2 nd ⁡ n ⟼ b m P n a ∧ ∀ p ∈ 1 st ⁡ m D Nat E 1 st ⁡ n ∀ q ∈ 2 nd ⁡ m C Nat D 2 nd ⁡ n p m P n q = x ∈ B ⟼ p m P n q ⁡ x ∧ ∀ x ∈ B p m P n q ⁡ x ∈ 1 st ⁡ O ⁡ m ⁡ x S 1 st ⁡ O ⁡ n ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x R y p m P n q ⁡ y 1 st ⁡ O ⁡ m ⁡ x 1 st ⁡ O ⁡ m ⁡ y ∙ ˙ 1 st ⁡ O ⁡ n ⁡ y x 2 nd ⁡ O ⁡ m y ⁡ h = x 2 nd ⁡ O ⁡ n y ⁡ h 1 st ⁡ O ⁡ m ⁡ x 1 st ⁡ O ⁡ n ⁡ x ∙ ˙ 1 st ⁡ O ⁡ n ⁡ y p m P n q ⁡ x ∧ ∀ x ∈ W ∀ t ∈ B x P x ⁡ I ⁡ x ⁡ t = K ⁡ 1 st ⁡ O ⁡ x ⁡ t ∧ ∀ y ∈ W ∀ z ∈ W ∀ m ∈ x H y ∀ n ∈ y H z ∀ t ∈ B x P z ⁡ n x y · ˙ z m ⁡ t = y P z ⁡ n ⁡ t 1 st ⁡ O ⁡ x ⁡ t 1 st ⁡ O ⁡ y ⁡ t ∙ ˙ 1 st ⁡ O ⁡ z ⁡ t x P y ⁡ m ⁡ t

Proof

Step Hyp Ref Expression
1 fucoisfunc.w ⊢ W = D Func E × C Func D
2 fucoisfunc2lem1.o ⊢ O = ∘ func ↾ W
3 fucoisfunc2lem1.b ⊢ B = Base C
4 fucoisfunc2lem1.r ⊢ R = Hom ⁡ C
5 fucoisfunc2lem1.s ⊢ S = Hom ⁡ E
6 fucoisfunc2lem1.v ⊢ ∙ ˙ = comp ⁡ E
7 fucoisfunc2.t ⊢ T = D FuncCat E × c C FuncCat D
8 fucoisfunc2.q ⊢ Q = C FuncCat E
9 fucoisfunc2.h ⊢ H = Hom ⁡ T
10 fucoisfunc2.i ⊢ I = Id ⁡ T
11 fucoisfunc2.x ⊢ · ˙ = comp ⁡ T
12 fucoisfunc2.c ⊢ φ → C ∈ Cat
13 fucoisfunc2.d ⊢ φ → D ∈ Cat
14 fucoisfunc2.e ⊢ φ → E ∈ Cat
15 fucoisfunc2.k ⊢ K = Id ⁡ E
16 eqid ⊢ Id ⁡ Q = Id ⁡ Q
17 eqid ⊢ comp ⁡ Q = comp ⁡ Q
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 fucoisfunc2lem2 ⊢ φ → O T Func Q P ↔ P = u ∈ W , v ∈ W ⟼ u P v ∧ ∀ m ∈ W ∀ n ∈ W m P n = b ∈ 1 st ⁡ m D Nat E 1 st ⁡ n , a ∈ 2 nd ⁡ m C Nat D 2 nd ⁡ n ⟼ b m P n a ∧ ∀ p ∈ 1 st ⁡ m D Nat E 1 st ⁡ n ∀ q ∈ 2 nd ⁡ m C Nat D 2 nd ⁡ n p m P n q = x ∈ B ⟼ p m P n q ⁡ x ∧ ∀ x ∈ B p m P n q ⁡ x ∈ 1 st ⁡ O ⁡ m ⁡ x S 1 st ⁡ O ⁡ n ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ h ∈ x R y p m P n q ⁡ y 1 st ⁡ O ⁡ m ⁡ x 1 st ⁡ O ⁡ m ⁡ y ∙ ˙ 1 st ⁡ O ⁡ n ⁡ y x 2 nd ⁡ O ⁡ m y ⁡ h = x 2 nd ⁡ O ⁡ n y ⁡ h 1 st ⁡ O ⁡ m ⁡ x 1 st ⁡ O ⁡ n ⁡ x ∙ ˙ 1 st ⁡ O ⁡ n ⁡ y p m P n q ⁡ x ∧ ∀ x ∈ W ∀ t ∈ B x P x ⁡ I ⁡ x ⁡ t = K ⁡ 1 st ⁡ O ⁡ x ⁡ t ∧ ∀ y ∈ W ∀ z ∈ W ∀ m ∈ x H y ∀ n ∈ y H z ∀ t ∈ B x P z ⁡ n x y · ˙ z m ⁡ t = y P z ⁡ n ⁡ t 1 st ⁡ O ⁡ x ⁡ t 1 st ⁡ O ⁡ y ⁡ t ∙ ˙ 1 st ⁡ O ⁡ z ⁡ t x P y ⁡ m ⁡ t