fucoisfunc2 - Mathbox for Zhi Wang

	Mathbox for Zhi Wang		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fucoisfunc2		Structured version Visualization version GIF version

Theorem fucoisfunc2 50581

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

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 50873 and fuconuniqex2 50878. (Contributed by Zhi Wang, 14-Sep-2026.) (Revised by Zhi Wang, 17-Sep-2026.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
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 ‘(𝑂‘𝑧))‘𝑡))(((𝑥𝑃𝑦)‘𝑚)‘𝑡))))))

Distinct variable groups: 𝐶,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧 𝐷,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧 𝐸,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧 𝑊,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧 𝑂,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧 𝑃,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧 𝐵,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,ℎ 𝑅,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,ℎ 𝑆,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,ℎ ∙ ,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,ℎ 𝐶,ℎ 𝐷,ℎ ℎ,𝐸 ℎ,𝑊 ℎ,𝑂 𝑃,ℎ 𝑇,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,𝑡,ℎ 𝑄,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,𝑡,ℎ 𝐻,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,𝑡,ℎ 𝐼,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,𝑡,ℎ 𝐾,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,𝑡,ℎ 𝜑,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,𝑡,ℎ · ,𝑎,𝑏,𝑚,𝑛,𝑝,𝑞,𝑢,𝑣,𝑥,𝑦,𝑧,𝑡,ℎ 𝑡,𝐵 𝑡,𝐶 𝑡,𝐷 𝑡,𝐸 𝑡,𝑊 𝑡,𝑂 𝑡,𝑃 𝑡,𝑅 𝑡,𝑆 𝑡, ∙

**Proof of Theorem fucoisfunc2**
Step	Hyp	Ref	Expression
1		fucoisfunc.w	. 2 ⊢ 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))
2		fucoisfunc2lem1.o	. 2 ⊢ 𝑂 = ( ∘_func ↾ 𝑊)
3		fucoisfunc2lem1.b	. 2 ⊢ 𝐵 = (Base‘𝐶)
4		fucoisfunc2lem1.r	. 2 ⊢ 𝑅 = (Hom ‘𝐶)
5		fucoisfunc2lem1.s	. 2 ⊢ 𝑆 = (Hom ‘𝐸)
6		fucoisfunc2lem1.v	. 2 ⊢ ∙ = (comp‘𝐸)
7		fucoisfunc2.t	. 2 ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×_c (𝐶 FuncCat 𝐷))
8		fucoisfunc2.q	. 2 ⊢ 𝑄 = (𝐶 FuncCat 𝐸)
9		fucoisfunc2.h	. 2 ⊢ 𝐻 = (Hom ‘𝑇)
10		fucoisfunc2.i	. 2 ⊢ 𝐼 = (Id‘𝑇)
11		fucoisfunc2.x	. 2 ⊢ · = (comp‘𝑇)
12		fucoisfunc2.c	. 2 ⊢ (𝜑 → 𝐶 ∈ Cat)
13		fucoisfunc2.d	. 2 ⊢ (𝜑 → 𝐷 ∈ Cat)
14		fucoisfunc2.e	. 2 ⊢ (𝜑 → 𝐸 ∈ Cat)
15		fucoisfunc2.k	. 2 ⊢ 𝐾 = (Id‘𝐸)
16		eqid 2760	. 2 ⊢ (Id‘𝑄) = (Id‘𝑄)
17		eqid 2760	. 2 ⊢ (comp‘𝑄) = (comp‘𝑄)
18	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17	fucoisfunc2lem2 50580	1 ⊢ (𝜑 → (𝑂(𝑇 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 ‘(𝑂‘𝑧))‘𝑡))(((𝑥𝑃𝑦)‘𝑚)‘𝑡))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ⟨cop 4589 class class class wbr 5102 ↦ cmpt 5185 × cxp 5648 ↾ cres 5652 ‘cfv 6538 (class class class)co 7420 ∈ cmpo 7422 1^st c1st 7999 2^nd c2nd 8000 Basecbs 17389 Hom chom 17441 compcco 17442 Catccat 17840 Idccid 17841 Func cfunc 18031 ∘_func ccofu 18033 Nat cnat 18121 FuncCat cfuc 18122 ×_c cxpc 18344

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11258 ax-resscn 11259 ax-1cn 11260 ax-icn 11261 ax-addcl 11262 ax-addrcl 11263 ax-mulcl 11264 ax-mulrcl 11265 ax-mulcom 11266 ax-addass 11267 ax-mulass 11268 ax-distr 11269 ax-i2m1 11270 ax-1ne0 11271 ax-1rid 11272 ax-rnegex 11273 ax-rrecex 11274 ax-cnre 11275 ax-pre-lttri 11276 ax-pre-lttrn 11277 ax-pre-ltadd 11278 ax-pre-mulgt0 11279

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8301 df-wrecs 8332 df-recs 8381 df-rdg 8420 df-1o 8478 df-er 8719 df-map 8851 df-ixp 8928 df-en 8976 df-dom 8977 df-sdom 8978 df-fin 8979 df-pnf 11347 df-mnf 11348 df-xr 11349 df-ltxr 11350 df-le 11351 df-sub 11545 df-neg 11546 df-nn 12338 df-2 12407 df-3 12408 df-4 12409 df-5 12410 df-6 12411 df-7 12412 df-8 12413 df-9 12414 df-n0 12609 df-z 12696 df-dec 12817 df-uz 12968 df-fz 13642 df-struct 17327 df-slot 17362 df-ndx 17374 df-base 17390 df-hom 17454 df-cco 17455 df-cat 17844 df-cid 17845 df-func 18035 df-cofu 18037 df-nat 18123 df-fuc 18124 df-xpc 18348

This theorem is used by: (None)

W3C validator