fuchom - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fuchom		Structured version Visualization version GIF version

Theorem fuchom 18054

Description: The morphisms in the functor category are natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.)

**Hypotheses**
Ref	Expression
fucbas.q	⊢ 𝑄 = (𝐶 FuncCat 𝐷)
fuchom.n	⊢ 𝑁 = (𝐶 Nat 𝐷)

**Assertion**
Ref	Expression
fuchom	⊢ 𝑁 = (Hom ‘𝑄)

Proof of Theorem fuchom Dummy variables 𝑎 𝑏 𝑓 𝑔 ℎ 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fucbas.q	. . . . 5 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
2		eqid 2760	. . . . 5 ⊢ (𝐶 Func 𝐷) = (𝐶 Func 𝐷)
3		fuchom.n	. . . . 5 ⊢ 𝑁 = (𝐶 Nat 𝐷)
4		eqid 2760	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2760	. . . . 5 ⊢ (comp‘𝐷) = (comp‘𝐷)
6		simpl 488	. . . . 5 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐶 ∈ Cat)
7		simpr 490	. . . . 5 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐷 ∈ Cat)
8		eqid 2760	. . . . . 6 ⊢ (comp‘𝑄) = (comp‘𝑄)
9	1, 2, 3, 4, 5, 6, 7, 8	fuccofval 18052	. . . . 5 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (comp‘𝑄) = (𝑣 ∈ ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)), ℎ ∈ (𝐶 Func 𝐷) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝐷)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))))
10	1, 2, 3, 4, 5, 6, 7, 9	fucval 18051	. . . 4 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑄 = {⟨(Base‘ndx), (𝐶 Func 𝐷)⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (comp‘𝑄)⟩})
11		catstr 18050	. . . 4 ⊢ {⟨(Base‘ndx), (𝐶 Func 𝐷)⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (comp‘𝑄)⟩} Struct ⟨1, ;15⟩
12		homid 17498	. . . 4 ⊢ Hom = Slot (Hom ‘ndx)
13		snsstp2 4778	. . . 4 ⊢ {⟨(Hom ‘ndx), 𝑁⟩} ⊆ {⟨(Base‘ndx), (𝐶 Func 𝐷)⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (comp‘𝑄)⟩}
14	3	ovexi 7448	. . . . 5 ⊢ 𝑁 ∈ V
15	14	a1i 11	. . . 4 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 ∈ V)
16		eqid 2760	. . . 4 ⊢ (Hom ‘𝑄) = (Hom ‘𝑄)
17	10, 11, 12, 13, 15, 16	strfv3 17297	. . 3 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (Hom ‘𝑄) = 𝑁)
18	17	eqcomd 2766	. 2 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 = (Hom ‘𝑄))
19	12	str0 17282	. . 3 ⊢ ∅ = (Hom ‘∅)
20	3	natffn 18042	. . . . 5 ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷))
21		funcrcl 17953	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
22	21	con3i 155	. . . . . . . . 9 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ¬ 𝑓 ∈ (𝐶 Func 𝐷))
23	22	eq0rdv 4365	. . . . . . . 8 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Func 𝐷) = ∅)
24	23	xpeq2d 5685	. . . . . . 7 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) = ((𝐶 Func 𝐷) × ∅))
25		xp0 5755	. . . . . . 7 ⊢ ((𝐶 Func 𝐷) × ∅) = ∅
26	24, 25	eqtrdi 2811	. . . . . 6 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) = ∅)
27	26	fneq2d 6627	. . . . 5 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) ↔ 𝑁 Fn ∅))
28	20, 27	mpbii 236	. . . 4 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 Fn ∅)
29		fn0 6664	. . . 4 ⊢ (𝑁 Fn ∅ ↔ 𝑁 = ∅)
30	28, 29	sylib 221	. . 3 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 = ∅)
31		fnfuc 18038	. . . . . . 7 ⊢ FuncCat Fn (Cat × Cat)
32	31	fndmi 6637	. . . . . 6 ⊢ dom FuncCat = (Cat × Cat)
33	32	ndmov 7599	. . . . 5 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 FuncCat 𝐷) = ∅)
34	1, 33	eqtrid 2807	. . . 4 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑄 = ∅)
35	34	fveq2d 6883	. . 3 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (Hom ‘𝑄) = (Hom ‘∅))
36	19, 30, 35	3eqtr4a 2821	. 2 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 = (Hom ‘𝑄))
37	18, 36	pm2.61i 184	1 ⊢ 𝑁 = (Hom ‘𝑄)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 ∧ wa 401 = wceq 1570 ∈ wcel 2145 Vcvv 3450 ∅c0 4279 {ctp 4588 ⟨cop 4590 × cxp 5653 Fn wfn 6528 ‘cfv 6533 (class class class)co 7414 1c1 11126 5c5 12323 cdc 12737 ndxcnx 17286 Basecbs 17302 Hom chom 17354 compcco 17355 Catccat 17753 Func cfunc 17944 Nat cnat 18034 FuncCat cfuc 18035

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 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202

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 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-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8456 df-er 8697 df-ixp 8906 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-6 12332 df-7 12333 df-8 12334 df-9 12335 df-n0 12530 df-z 12617 df-dec 12738 df-uz 12889 df-fz 13563 df-struct 17240 df-slot 17275 df-ndx 17287 df-base 17303 df-hom 17367 df-cco 17368 df-func 17948 df-nat 18036 df-fuc 18037

This theorem is used by: fuccatid 18062 fucsect 18065 fuciso 18068 evlfcllem 18310 evlfcl 18311 curfcl 18321 uncf2 18326 curfuncf 18327 diag2cl 18335 curf2ndf 18336 yonedalem21 18362 yonedalem22 18367 yonedalem3b 18368 yonedalem3 18369 yonffthlem 18371 xpcfuchomfval 50180 xpcfuchom 50181 xpcfuchom2 50182 xpcfucco2 50183 diag2f1 50236 fucoid 50275 fucofunc 50286 postcofval 50291 precofval 50294 precofvalALT 50295 fucoppcco 50336 fucoppc 50337 oppfdiag 50343 diagffth 50465 funcsn 50468 0fucterm 50470 lanrcl5 50562 ranrcl5 50567 lanup 50568 ranup 50569 islmd 50592 iscmd 50593 lmddu 50594

W3C validator