fucoco2 - Mathbox for Zhi Wang

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

Theorem fucoco2 50286

Description: Composition in the source category is mapped to composition in the target. See also fucoco 50285. (Contributed by Zhi Wang, 3-Oct-2025.)

**Hypotheses**
Ref	Expression
fucoco2.t	⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×_c (𝐶 FuncCat 𝐷))
fucoco2.q	⊢ 𝑄 = (𝐶 FuncCat 𝐸)
fucoco2.o	⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘_F 𝐸) = ⟨𝑂, 𝑃⟩)
fucoco2.1	⊢ · = (comp‘𝑇)
fucoco2.2	⊢ ∙ = (comp‘𝑄)
fucoco2.w	⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
fucoco2.x	⊢ (𝜑 → 𝑋 ∈ 𝑊)
fucoco2.y	⊢ (𝜑 → 𝑌 ∈ 𝑊)
fucoco2.z	⊢ (𝜑 → 𝑍 ∈ 𝑊)
fucoco2.j	⊢ 𝐽 = (Hom ‘𝑇)
fucoco2.a	⊢ (𝜑 → 𝐴 ∈ (𝑋𝐽𝑌))
fucoco2.b	⊢ (𝜑 → 𝐵 ∈ (𝑌𝐽𝑍))

**Assertion**
Ref	Expression
fucoco2	⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))

**Proof of Theorem fucoco2**
Step	Hyp	Ref	Expression
1		fucoco2.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐽𝑌))
2		fucoco2.t	. . . . 5 ⊢ 𝑇 = ((𝐷 FuncCat 𝐸) ×_c (𝐶 FuncCat 𝐷))
3	2	xpcfucbas 50180	. . . . 5 ⊢ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) = (Base‘𝑇)
4		fucoco2.j	. . . . 5 ⊢ 𝐽 = (Hom ‘𝑇)
5		fucoco2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑊)
6		fucoco2.w	. . . . . 6 ⊢ (𝜑 → 𝑊 = ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
7	5, 6	eleqtrd 2864	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
8		fucoco2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑊)
9	8, 6	eleqtrd 2864	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
10	2, 3, 4, 7, 9	xpcfuchom 50182	. . . 4 ⊢ (𝜑 → (𝑋𝐽𝑌) = (((1^st ‘𝑋)(𝐷 Nat 𝐸)(1^st ‘𝑌)) × ((2^nd ‘𝑋)(𝐶 Nat 𝐷)(2^nd ‘𝑌))))
11	1, 10	eleqtrd 2864	. . 3 ⊢ (𝜑 → 𝐴 ∈ (((1^st ‘𝑋)(𝐷 Nat 𝐸)(1^st ‘𝑌)) × ((2^nd ‘𝑋)(𝐶 Nat 𝐷)(2^nd ‘𝑌))))
12		xp1st 8021	. . 3 ⊢ (𝐴 ∈ (((1^st ‘𝑋)(𝐷 Nat 𝐸)(1^st ‘𝑌)) × ((2^nd ‘𝑋)(𝐶 Nat 𝐷)(2^nd ‘𝑌))) → (1^st ‘𝐴) ∈ ((1^st ‘𝑋)(𝐷 Nat 𝐸)(1^st ‘𝑌)))
13	11, 12	syl 18	. 2 ⊢ (𝜑 → (1^st ‘𝐴) ∈ ((1^st ‘𝑋)(𝐷 Nat 𝐸)(1^st ‘𝑌)))
14		xp2nd 8022	. . 3 ⊢ (𝐴 ∈ (((1^st ‘𝑋)(𝐷 Nat 𝐸)(1^st ‘𝑌)) × ((2^nd ‘𝑋)(𝐶 Nat 𝐷)(2^nd ‘𝑌))) → (2^nd ‘𝐴) ∈ ((2^nd ‘𝑋)(𝐶 Nat 𝐷)(2^nd ‘𝑌)))
15	11, 14	syl 18	. 2 ⊢ (𝜑 → (2^nd ‘𝐴) ∈ ((2^nd ‘𝑋)(𝐶 Nat 𝐷)(2^nd ‘𝑌)))
16		fucoco2.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝑌𝐽𝑍))
17		fucoco2.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑊)
18	17, 6	eleqtrd 2864	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)))
19	2, 3, 4, 9, 18	xpcfuchom 50182	. . . 4 ⊢ (𝜑 → (𝑌𝐽𝑍) = (((1^st ‘𝑌)(𝐷 Nat 𝐸)(1^st ‘𝑍)) × ((2^nd ‘𝑌)(𝐶 Nat 𝐷)(2^nd ‘𝑍))))
20	16, 19	eleqtrd 2864	. . 3 ⊢ (𝜑 → 𝐵 ∈ (((1^st ‘𝑌)(𝐷 Nat 𝐸)(1^st ‘𝑍)) × ((2^nd ‘𝑌)(𝐶 Nat 𝐷)(2^nd ‘𝑍))))
21		xp1st 8021	. . 3 ⊢ (𝐵 ∈ (((1^st ‘𝑌)(𝐷 Nat 𝐸)(1^st ‘𝑍)) × ((2^nd ‘𝑌)(𝐶 Nat 𝐷)(2^nd ‘𝑍))) → (1^st ‘𝐵) ∈ ((1^st ‘𝑌)(𝐷 Nat 𝐸)(1^st ‘𝑍)))
22	20, 21	syl 18	. 2 ⊢ (𝜑 → (1^st ‘𝐵) ∈ ((1^st ‘𝑌)(𝐷 Nat 𝐸)(1^st ‘𝑍)))
23		xp2nd 8022	. . 3 ⊢ (𝐵 ∈ (((1^st ‘𝑌)(𝐷 Nat 𝐸)(1^st ‘𝑍)) × ((2^nd ‘𝑌)(𝐶 Nat 𝐷)(2^nd ‘𝑍))) → (2^nd ‘𝐵) ∈ ((2^nd ‘𝑌)(𝐶 Nat 𝐷)(2^nd ‘𝑍)))
24	20, 23	syl 18	. 2 ⊢ (𝜑 → (2^nd ‘𝐵) ∈ ((2^nd ‘𝑌)(𝐶 Nat 𝐷)(2^nd ‘𝑍)))
25		fucoco2.o	. 2 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘_F 𝐸) = ⟨𝑂, 𝑃⟩)
26		1st2nd2 8028	. . 3 ⊢ (𝑋 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) → 𝑋 = ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩)
27	7, 26	syl 18	. 2 ⊢ (𝜑 → 𝑋 = ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩)
28		1st2nd2 8028	. . 3 ⊢ (𝑌 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) → 𝑌 = ⟨(1^st ‘𝑌), (2^nd ‘𝑌)⟩)
29	9, 28	syl 18	. 2 ⊢ (𝜑 → 𝑌 = ⟨(1^st ‘𝑌), (2^nd ‘𝑌)⟩)
30		1st2nd2 8028	. . 3 ⊢ (𝑍 ∈ ((𝐷 Func 𝐸) × (𝐶 Func 𝐷)) → 𝑍 = ⟨(1^st ‘𝑍), (2^nd ‘𝑍)⟩)
31	18, 30	syl 18	. 2 ⊢ (𝜑 → 𝑍 = ⟨(1^st ‘𝑍), (2^nd ‘𝑍)⟩)
32		1st2nd2 8028	. . 3 ⊢ (𝐴 ∈ (((1^st ‘𝑋)(𝐷 Nat 𝐸)(1^st ‘𝑌)) × ((2^nd ‘𝑋)(𝐶 Nat 𝐷)(2^nd ‘𝑌))) → 𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩)
33	11, 32	syl 18	. 2 ⊢ (𝜑 → 𝐴 = ⟨(1^st ‘𝐴), (2^nd ‘𝐴)⟩)
34		1st2nd2 8028	. . 3 ⊢ (𝐵 ∈ (((1^st ‘𝑌)(𝐷 Nat 𝐸)(1^st ‘𝑍)) × ((2^nd ‘𝑌)(𝐶 Nat 𝐷)(2^nd ‘𝑍))) → 𝐵 = ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩)
35	20, 34	syl 18	. 2 ⊢ (𝜑 → 𝐵 = ⟨(1^st ‘𝐵), (2^nd ‘𝐵)⟩)
36		fucoco2.q	. 2 ⊢ 𝑄 = (𝐶 FuncCat 𝐸)
37		fucoco2.2	. 2 ⊢ ∙ = (comp‘𝑄)
38		fucoco2.1	. 2 ⊢ · = (comp‘𝑇)
39	13, 15, 22, 24, 25, 27, 29, 31, 33, 35, 36, 37, 2, 38	fucoco 50285	1 ⊢ (𝜑 → ((𝑋𝑃𝑍)‘(𝐵(⟨𝑋, 𝑌⟩ · 𝑍)𝐴)) = (((𝑌𝑃𝑍)‘𝐵)(⟨(𝑂‘𝑋), (𝑂‘𝑌)⟩ ∙ (𝑂‘𝑍))((𝑋𝑃𝑌)‘𝐴)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2145 ⟨cop 4593 × cxp 5657 ‘cfv 6537 (class class class)co 7416 1^st c1st 7987 2^nd c2nd 7988 Hom chom 17357 compcco 17358 Func cfunc 17947 Nat cnat 18037 FuncCat cfuc 18038 ×_c cxpc 18260 ∘_F cfuco 50244

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-er 8699 df-map 8831 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-fz 13564 df-struct 17243 df-slot 17278 df-ndx 17290 df-base 17306 df-hom 17370 df-cco 17371 df-cat 17760 df-cid 17761 df-func 17951 df-cofu 17953 df-nat 18039 df-fuc 18040 df-xpc 18264 df-fuco 50245

This theorem is used by: fucofunc 50287

W3C validator