Theorem funcid 17837

Description: A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
funcid.b	⊢ 𝐵 = (Base‘𝐷)
funcid.1	⊢ 1 = (Id‘𝐷)
funcid.i	⊢ 𝐼 = (Id‘𝐸)
funcid.f	⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
funcid.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Assertion

Ref	Expression
funcid	⊢ (𝜑 → ((𝑋𝐺𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝐹‘𝑋)))

Proof of Theorem funcid

Dummy variables 𝑚 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . . . 5 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
2	1, 1	oveq12d 7385	. . . 4 ⊢ (𝑥 = 𝑋 → (𝑥𝐺𝑥) = (𝑋𝐺𝑋))
3		fveq2 6841	. . . 4 ⊢ (𝑥 = 𝑋 → ( 1 ‘𝑥) = ( 1 ‘𝑋))
4	2, 3	fveq12d 6848	. . 3 ⊢ (𝑥 = 𝑋 → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = ((𝑋𝐺𝑋)‘( 1 ‘𝑋)))
5		2fveq3 6846	. . 3 ⊢ (𝑥 = 𝑋 → (𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑋)))
6	4, 5	eqeq12d 2753	. 2 ⊢ (𝑥 = 𝑋 → (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ↔ ((𝑋𝐺𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝐹‘𝑋))))
7		funcid.f	. . . . 5 ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
8		funcid.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐷)
9		eqid 2737	. . . . . 6 ⊢ (Base‘𝐸) = (Base‘𝐸)
10		eqid 2737	. . . . . 6 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
11		eqid 2737	. . . . . 6 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
12		funcid.1	. . . . . 6 ⊢ 1 = (Id‘𝐷)
13		funcid.i	. . . . . 6 ⊢ 𝐼 = (Id‘𝐸)
14		eqid 2737	. . . . . 6 ⊢ (comp‘𝐷) = (comp‘𝐷)
15		eqid 2737	. . . . . 6 ⊢ (comp‘𝐸) = (comp‘𝐸)
16		df-br 5087	. . . . . . . . 9 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
17	7, 16	sylib 218	. . . . . . . 8 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
18		funcrcl 17830	. . . . . . . 8 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
19	17, 18	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
20	19	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ Cat)
21	19	simprd 495	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ Cat)
22	8, 9, 10, 11, 12, 13, 14, 15, 20, 21	isfunc 17831	. . . . 5 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
23	7, 22	mpbid 232	. . . 4 ⊢ (𝜑 → (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
24	23	simp3d 1145	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
25		simpl 482	. . . 4 ⊢ ((((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
26	25	ralimi 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) → ∀𝑥 ∈ 𝐵 ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
27	24, 26	syl 17	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
28		funcid.x	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29	6, 27, 28	rspcdva 3566	1 ⊢ (𝜑 → ((𝑋𝐺𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝐹‘𝑋)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ⟨cop 4574   class class class wbr 5086   × cxp 5629  ⟶wf 6495  ‘cfv 6499  (class class class)co 7367  1^st c1st 7940  2^nd c2nd 7941   ↑_m cmap 8773  Xcixp 8845  Basecbs 17179  Hom chom 17231  compcco 17232  Catccat 17630  Idccid 17631   Func cfunc 17821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7370  df-oprab 7371  df-mpo 7372  df-map 8775  df-ixp 8846  df-func 17825

This theorem is referenced by:  funcsect  17839  funcoppc  17842  cofucl  17855  funcres  17863  fthsect  17894  catcisolem  18077  prfcl  18169  evlfcl  18188  curf1cl  18194  curfcl  18198  curfuncf  18204  yonedainv  18247  imaid  49623  upciclem3  49637  fucoid  49817  fucorid  49831  precofvallem  49835  termcfuncval  50001