fucid - Metamath Proof Explorer

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

Theorem fucid 18190

Description: The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)

**Hypotheses**
Ref	Expression
fucid.q	⊢ 𝑄 = (𝐶 FuncCat 𝐷)
fucid.i	⊢ 𝐼 = (Id‘𝑄)
fucid.1	⊢ 1 = (Id‘𝐷)
fucid.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))

**Assertion**
Ref	Expression
fucid	⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1^st ‘𝐹)))

Proof of Theorem fucid Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fucid.i	. . 3 ⊢ 𝐼 = (Id‘𝑄)
2		fucid.q	. . . . 5 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
3		fucid.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
4		funcrcl 18079	. . . . . . 7 ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
5	3, 4	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
6	5	simpld 500	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ Cat)
7	5	simprd 501	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ Cat)
8		fucid.1	. . . . 5 ⊢ 1 = (Id‘𝐷)
9	2, 6, 7, 8	fuccatid 18188	. . . 4 ⊢ (𝜑 → (𝑄 ∈ Cat ∧ (Id‘𝑄) = (𝑓 ∈ (𝐶 Func 𝐷) ↦ ( 1 ∘ (1^st ‘𝑓)))))
10	9	simprd 501	. . 3 ⊢ (𝜑 → (Id‘𝑄) = (𝑓 ∈ (𝐶 Func 𝐷) ↦ ( 1 ∘ (1^st ‘𝑓))))
11	1, 10	eqtrid 2810	. 2 ⊢ (𝜑 → 𝐼 = (𝑓 ∈ (𝐶 Func 𝐷) ↦ ( 1 ∘ (1^st ‘𝑓))))
12		simpr 490	. . . 4 ⊢ ((𝜑 ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹)
13	12	fveq2d 6918	. . 3 ⊢ ((𝜑 ∧ 𝑓 = 𝐹) → (1^st ‘𝑓) = (1^st ‘𝐹))
14	13	coeq2d 5849	. 2 ⊢ ((𝜑 ∧ 𝑓 = 𝐹) → ( 1 ∘ (1^st ‘𝑓)) = ( 1 ∘ (1^st ‘𝐹)))
15	8	fvexi 6928	. . . 4 ⊢ 1 ∈ V
16		fvex 6927	. . . 4 ⊢ (1^st ‘𝐹) ∈ V
17	15, 16	coex 7974	. . 3 ⊢ ( 1 ∘ (1^st ‘𝐹)) ∈ V
18	17	a1i 11	. 2 ⊢ (𝜑 → ( 1 ∘ (1^st ‘𝐹)) ∈ V)
19	11, 14, 3, 18	fvmptd 7030	1 ⊢ (𝜑 → (𝐼‘𝐹) = ( 1 ∘ (1^st ‘𝐹)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 Vcvv 3454 ↦ cmpt 5190 ∘ ccom 5660 ‘cfv 6564 (class class class)co 7449 1^st c1st 8031 Catccat 17879 Idccid 17880 Func cfunc 18070 FuncCat cfuc 18161

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-om 7910 df-1st 8033 df-2nd 8034 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-er 8753 df-map 8885 df-ixp 8962 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-nn 12374 df-2 12443 df-3 12444 df-4 12445 df-5 12446 df-6 12447 df-7 12448 df-8 12449 df-9 12450 df-n0 12645 df-z 12732 df-dec 12853 df-uz 13004 df-fz 13678 df-struct 17366 df-slot 17401 df-ndx 17413 df-base 17429 df-hom 17493 df-cco 17494 df-cat 17883 df-cid 17884 df-func 18074 df-nat 18162 df-fuc 18163

This theorem is used by: fucsect 18191 evlfcl 18437 curfcl 18447 curfuncf 18453 curf2ndf 18462 natideq 50670 fuco11id 50781 fucoid 50795 fucolid 50808 fucorid 50809 precofvalALT 50828 fucoppcid 50868

W3C validator