fucofunc - Mathbox for Zhi Wang

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

Theorem fucofunc 49944

Description: The functor composition bifunctor is a functor. See also fucofunca 49945.

However, it is unlikely the unique functor compatible with the functor composition. As a counterexample, let 𝐶 and 𝐷 be terminal categories (categories of one object and one morphism, df-termc 50058), for example, (SetCat‘1_o) (the trivial category, setc1oterm 50076), and 𝐸 be a category with two objects equipped with only two non-identity morphisms 𝑓 and 𝑔, pointing in the same direction. It is possible to map the ordered pair of natural transformations ⟨𝑎, 𝑖⟩, where 𝑎 sends to 𝑓 and 𝑖 is the identity natural transformation, to the other natural transformation 𝑏 sending to 𝑔, i.e., define the morphism part 𝑃 such that (𝑎(𝑈𝑃𝑉)𝑖) = 𝑏 such that (𝑏‘𝑋) = 𝑔 given hypotheses of fuco23 49926. Such construction should be provable as a functor.

Given any 𝑃, it is a morphism part of a functor compatible with the object part, i.e., the functor composition, i.e., the restriction of ∘_func, iff both of the following hold.

1. It has the same form as df-fuco 49902 up to fuco23 49926, but ((𝐵(𝑈𝑃𝑉)𝐴)‘𝑋) might be mapped to a different morphism in category 𝐸. See fucofulem2 49896 for some insights.

2. fuco22nat 49931, fucoid 49933, and fucoco 49942 are satisfied.

(Contributed by Zhi Wang, 3-Oct-2025.)

**Hypotheses**
Ref	Expression
fucoco2.t	⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×_c (𝐶 FuncCat 𝐷))
fucoco2.q	⊢ 𝑄 = (𝐶 FuncCat 𝐸)
fucoco2.o	⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘_F 𝐸) = ⟨𝑂, 𝑃⟩)
fucofunc.c	⊢ (𝜑 → 𝐶 ∈ Cat)
fucofunc.d	⊢ (𝜑 → 𝐷 ∈ Cat)
fucofunc.e	⊢ (𝜑 → 𝐸 ∈ Cat)

**Assertion**
Ref	Expression
fucofunc	⊢ (𝜑 → 𝑂(𝑇 Func 𝑄)𝑃)

Proof of Theorem fucofunc Dummy variables 𝑚 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fucoco2.t	. . 3 ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×_c (𝐶 FuncCat 𝐷))
2	1	xpcfucbas 49837	. 2 ⊢ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) = (Base‘𝑇)
3		fucoco2.q	. . 3 ⊢ 𝑄 = (𝐶 FuncCat 𝐸)
4	3	fucbas 17979	. 2 ⊢ (𝐶 Func 𝐸) = (Base‘𝑄)
5		eqid 2761	. 2 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
6		eqid 2761	. . 3 ⊢ (𝐶 Nat 𝐸) = (𝐶 Nat 𝐸)
7	3, 6	fuchom 17980	. 2 ⊢ (𝐶 Nat 𝐸) = (Hom ‘𝑄)
8		eqid 2761	. 2 ⊢ (Id‘𝑇) = (Id‘𝑇)
9		eqid 2761	. 2 ⊢ (Id‘𝑄) = (Id‘𝑄)
10		eqid 2761	. 2 ⊢ (comp‘𝑇) = (comp‘𝑇)
11		eqid 2761	. 2 ⊢ (comp‘𝑄) = (comp‘𝑄)
12		eqid 2761	. . . 4 ⊢ (𝐷 FuncCat 𝐸) = (𝐷 FuncCat 𝐸)
13		fucofunc.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
14		fucofunc.e	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
15	12, 13, 14	fuccat 17989	. . 3 ⊢ (𝜑 → (𝐷 FuncCat 𝐸) ∈ Cat)
16		eqid 2761	. . . 4 ⊢ (𝐶 FuncCat 𝐷) = (𝐶 FuncCat 𝐷)
17		fucofunc.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
18	16, 17, 13	fuccat 17989	. . 3 ⊢ (𝜑 → (𝐶 FuncCat 𝐷) ∈ Cat)
19	1, 15, 18	xpccat 18205	. 2 ⊢ (𝜑 → 𝑇 ∈ Cat)
20	3, 17, 14	fuccat 17989	. 2 ⊢ (𝜑 → 𝑄 ∈ Cat)
21		fucoco2.o	. . 3 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘_F 𝐸) = ⟨𝑂, 𝑃⟩)
22		eqidd 2762	. . 3 ⊢ (𝜑 → ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
23	17, 13, 14, 21, 22	fucof1 49907	. 2 ⊢ (𝜑 → 𝑂:((𝐷 Func 𝐸) × (𝐶 Func 𝐷))⟶(𝐶 Func 𝐸))
24	17, 13, 14, 21, 22	fucofn2 49909	. 2 ⊢ (𝜑 → 𝑃 Fn (((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) × ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))))
25	21	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))) → (⟨𝐶, 𝐷⟩ ∘_F 𝐸) = ⟨𝑂, 𝑃⟩)
26		eqidd 2762	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))) → ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
27		simprl 780	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))) → 𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
28		simprr 782	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))) → 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
29	25, 1, 5, 26, 27, 28	fucof21 49932	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))) → (𝑥𝑃𝑦):(𝑥(Hom ‘𝑇)𝑦)⟶((𝑂‘𝑥)(𝐶 Nat 𝐸)(𝑂‘𝑦)))
30	21	adantr 484	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) → (⟨𝐶, 𝐷⟩ ∘_F 𝐸) = ⟨𝑂, 𝑃⟩)
31		eqidd 2762	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) → ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
32		simpr 488	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) → 𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
33	30, 1, 8, 3, 9, 31, 32	fucoid2 49934	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) → ((𝑥𝑃𝑥)‘((Id‘𝑇)‘𝑥)) = ((Id‘𝑄)‘(𝑂‘𝑥)))
34	21	3ad2ant1 1145	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ∧ (𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (⟨𝐶, 𝐷⟩ ∘_F 𝐸) = ⟨𝑂, 𝑃⟩)
35		eqidd 2762	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ∧ (𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
36		simp21 1219	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ∧ (𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
37		simp22 1220	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ∧ (𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
38		simp23 1221	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ∧ (𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
39		simp3l 1214	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ∧ (𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦))
40		simp3r 1215	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ∧ (𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))
41	1, 3, 34, 10, 11, 35, 36, 37, 38, 5, 39, 40	fucoco2 49943	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑦 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) ∧ 𝑧 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷))) ∧ (𝑚 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑛 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥𝑃𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑚)) = (((𝑦𝑃𝑧)‘𝑛)(⟨(𝑂‘𝑥), (𝑂‘𝑦)⟩(comp‘𝑄)(𝑂‘𝑧))((𝑥𝑃𝑦)‘𝑚)))
42	2, 4, 5, 7, 8, 9, 10, 11, 19, 20, 23, 24, 29, 33, 41	isfuncd 17881	1 ⊢ (𝜑 → 𝑂(𝑇 Func 𝑄)𝑃)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ⟨cop 4587 class class class wbr 5099 × cxp 5643 ‘cfv 6517 (class class class)co 7392 Hom chom 17280 compcco 17281 Catccat 17679 Idccid 17680 Func cfunc 17870 Nat cnat 17960 FuncCat cfuc 17961 ×_c cxpc 18183 ∘_F cfuco 49901

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-om 7843 df-1st 7966 df-2nd 7967 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-er 8673 df-map 8805 df-ixp 8876 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-nn 12208 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12479 df-z 12566 df-dec 12686 df-uz 12837 df-fz 13510 df-struct 17166 df-slot 17201 df-ndx 17213 df-base 17229 df-hom 17293 df-cco 17294 df-cat 17683 df-cid 17684 df-func 17874 df-cofu 17876 df-nat 17962 df-fuc 17963 df-xpc 18187 df-fuco 49902

This theorem is referenced by: fucofunca 49945

W3C validator