Theorem funcf1 17831

Description: The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
funcf1.b	⊢ 𝐵 = (Base‘𝐷)
funcf1.c	⊢ 𝐶 = (Base‘𝐸)
funcf1.f	⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)

Assertion

Ref	Expression
funcf1	⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

Proof of Theorem funcf1

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

Step	Hyp	Ref	Expression
1		funcf1.f	. . 3 ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
2		funcf1.b	. . . 4 ⊢ 𝐵 = (Base‘𝐷)
3		funcf1.c	. . . 4 ⊢ 𝐶 = (Base‘𝐸)
4		eqid 2740	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2740	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2740	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2740	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2740	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2740	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 5080	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 219	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 17828	. . . . . 6 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
14	13	simpld 495	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
15	13	simprd 496	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
16	2, 3, 4, 5, 6, 7, 8, 9, 14, 15	isfunc 17829	. . 3 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
17	1, 16	mpbid 233	. 2 ⊢ (𝜑 → (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
18	17	simp1d 1148	1 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ⟨cop 4568   class class class wbr 5079   × cxp 5623  ⟶wf 6488  ‘cfv 6492  (class class class)co 7363  1^st c1st 7936  2^nd c2nd 7937   ↑_m cmap 8770  Xcixp 8842  Basecbs 17177  Hom chom 17229  compcco 17230  Catccat 17628  Idccid 17629   Func cfunc 17819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-map 8772  df-ixp 8843  df-func 17823

This theorem is referenced by:  funcsect  17837  funcinv  17838  funciso  17839  funcoppc  17840  cofu1  17849  cofucl  17853  cofuass  17854  cofulid  17855  cofurid  17856  funcres  17861  funcres2  17863  wunfunc  17866  funcres2c  17868  fullpropd  17887  fthsect  17892  fthinv  17893  fthmon  17894  ffthiso  17896  cofull  17901  cofth  17902  fuccocl  17932  fucidcl  17933  fuclid  17934  fucrid  17935  fucass  17936  fucsect  17940  fucinv  17941  invfuc  17942  fuciso  17943  natpropd  17944  fucpropd  17945  catciso  18076  prfval  18163  prfcl  18167  prf1st  18168  prf2nd  18169  1st2ndprf  18170  evlfcllem  18185  evlfcl  18186  curf1cl  18192  curfcl  18196  uncf1  18200  uncf2  18201  curfuncf  18202  uncfcurf  18203  diag1cl  18206  curf2ndf  18211  yon1cl  18227  oyon1cl  18235  yonedalem3a  18238  yonedalem4c  18241  yonedalem3b  18243  yonedalem3  18244  yonedainv  18245  yonffthlem  18246  yoniso  18249  func0g  49586  funchomf  49594  cofidf2a  49614  cofidf1a  49615  cofidf1  49618  imasubc  49648  imassc  49650  imaid  49651  imasubc3  49653  upciclem2  49664  upciclem3  49665  upeu2  49669  uppropd  49678  oppcup  49704  uptrlem1  49707  uptrlem3  49709  uptrar  49713  natoppf  49726  diag1  49801  diag1f1  49804  fuco111x  49828  fuco11idx  49832  fuco22natlem1  49839  fuco22natlem2  49840  fuco22natlem3  49841  fuco22natlem  49842  fucoid  49845  fuco23alem  49848  fucocolem1  49850  fucocolem2  49851  fucocolem3  49852  fucocolem4  49853  fucoco  49854  fucolid  49858  fucorid  49859  fucorid2  49860  precofvallem  49863  precofvalALT  49865  precofval2  49866  prcof22a  49889  prcofdiag1  49890  prcofdiag  49891  fucoppcco  49906  oppfdiag1  49911  oppfdiag  49913  functhincfun  49946  fullthinc  49947  thincciso2  49952  functermc  50005  fulltermc  50008  termcfuncval  50029  funcsn  50038  uobeqterm  50043  concom  50160  coccom  50161