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 18148

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 18146	. . . . 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 18145	. . . 4 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑄 = {⟨(Base‘ndx), (𝐶 Func 𝐷)⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (comp‘𝑄)⟩})
11		catstr 18144	. . . 4 ⊢ {⟨(Base‘ndx), (𝐶 Func 𝐷)⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (comp‘𝑄)⟩} Struct ⟨1, ;15⟩
12		homid 17592	. . . 4 ⊢ Hom = Slot (Hom ‘ndx)
13		snsstp2 4772	. . . 4 ⊢ {⟨(Hom ‘ndx), 𝑁⟩} ⊆ {⟨(Base‘ndx), (𝐶 Func 𝐷)⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (comp‘𝑄)⟩}
14	3	ovexi 7458	. . . . 5 ⊢ 𝑁 ∈ V
15	14	a1i 11	. . . 4 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 ∈ V)
16		eqid 2760	. . . 4 ⊢ (Hom ‘𝑄) = (Hom ‘𝑄)
17	10, 11, 12, 13, 15, 16	strfv3 17391	. . 3 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (Hom ‘𝑄) = 𝑁)
18	17	eqcomd 2766	. 2 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 = (Hom ‘𝑄))
19	12	str0 17376	. . 3 ⊢ ∅ = (Hom ‘∅)
20	3	natffn 18136	. . . . 5 ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷))
21		funcrcl 18047	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
22	21	con3i 155	. . . . . . . . 9 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ¬ 𝑓 ∈ (𝐶 Func 𝐷))
23	22	eq0rdv 4364	. . . . . . . 8 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Func 𝐷) = ∅)
24	23	xpeq2d 5681	. . . . . . 7 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) = ((𝐶 Func 𝐷) × ∅))
25		xp0 5752	. . . . . . 7 ⊢ ((𝐶 Func 𝐷) × ∅) = ∅
26	24, 25	eqtrdi 2811	. . . . . 6 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) = ∅)
27	26	fneq2d 6638	. . . . 5 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) ↔ 𝑁 Fn ∅))
28	20, 27	mpbii 236	. . . 4 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 Fn ∅)
29		fn0 6675	. . . 4 ⊢ (𝑁 Fn ∅ ↔ 𝑁 = ∅)
30	28, 29	sylib 221	. . 3 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑁 = ∅)
31		fnfuc 18132	. . . . . . 7 ⊢ FuncCat Fn (Cat × Cat)
32	31	fndmi 6648	. . . . . 6 ⊢ dom FuncCat = (Cat × Cat)
33	32	ndmov 7609	. . . . 5 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 FuncCat 𝐷) = ∅)
34	1, 33	eqtrid 2807	. . . 4 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝑄 = ∅)
35	34	fveq2d 6894	. . 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 1569 ∈ wcel 2144 Vcvv 3450 ∅c0 4277 {ctp 4588 ⟨cop 4834 × cxp 5649 Fn wfn 6538 ‘cfv 6543 (class class class)co 7424 1c1 11208 5c5 12407 cdc 12821 ndxcnx 17380 Basecbs 17396 Hom chom 17448 compcco 17449 Catccat 17847 Func cfunc 18038 Nat cnat 18128 FuncCat cfuc 18129

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 5327 ax-pr 5391 ax-un 7755 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284

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-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7882 df-1st 8005 df-2nd 8006 df-frecs 8307 df-wrecs 8338 df-recs 8387 df-rdg 8426 df-1o 8484 df-er 8725 df-ixp 8934 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-nn 12343 df-2 12412 df-3 12413 df-4 12414 df-5 12415 df-6 12416 df-7 12417 df-8 12418 df-9 12419 df-n0 12614 df-z 12701 df-dec 12822 df-uz 12973 df-fz 13647 df-struct 17334 df-slot 17369 df-ndx 17381 df-base 17397 df-hom 17461 df-cco 17462 df-func 18042 df-nat 18130 df-fuc 18131

This theorem is used by: fuccatid 18156 fucsect 18159 fuciso 18162 evlfcllem 18404 evlfcl 18405 curfcl 18415 uncf2 18420 curfuncf 18421 diag2cl 18429 curf2ndf 18430 yonedalem21 18456 yonedalem22 18461 yonedalem3b 18462 yonedalem3 18463 yonffthlem 18465 xpcfuchomfval 50511 xpcfuchom 50512 xpcfuchom2 50513 xpcfucco2 50514 diag2f1 50567 fucoid 50606 fucofunc 50617 fucoisfunc 50623 fucoaltvallem 50628 postcofval 50632 precofval 50638 precofvalALT 50639 fucoppcco 50680 fucoppc 50681 oppfdiag 50687 diagffth 50812 funcsn 50815 0fucterm 50817 lanrcl5 50954 ranrcl5 50959 lanup 50960 ranup 50961 islmd 50984 iscmd 50985 lmddu 50986

W3C validator