Theorem funcf1 17802

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 2737	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2737	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2737	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2737	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2737	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2737	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 5101	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 218	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 17799	. . . . . 6 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
14	13	simpld 494	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
15	13	simprd 495	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
16	2, 3, 4, 5, 6, 7, 8, 9, 14, 15	isfunc 17800	. . 3 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
17	1, 16	mpbid 232	. 2 ⊢ (𝜑 → (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
18	17	simp1d 1143	1 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ⟨cop 4588   class class class wbr 5100   × cxp 5630  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  1^st c1st 7941  2^nd c2nd 7942   ↑_m cmap 8775  Xcixp 8847  Basecbs 17148  Hom chom 17200  compcco 17201  Catccat 17599  Idccid 17600   Func cfunc 17790

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 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-map 8777  df-ixp 8848  df-func 17794

This theorem is referenced by:  funcsect  17808  funcinv  17809  funciso  17810  funcoppc  17811  cofu1  17820  cofucl  17824  cofuass  17825  cofulid  17826  cofurid  17827  funcres  17832  funcres2  17834  wunfunc  17837  funcres2c  17839  fullpropd  17858  fthsect  17863  fthinv  17864  fthmon  17865  ffthiso  17867  cofull  17872  cofth  17873  fuccocl  17903  fucidcl  17904  fuclid  17905  fucrid  17906  fucass  17907  fucsect  17911  fucinv  17912  invfuc  17913  fuciso  17914  natpropd  17915  fucpropd  17916  catciso  18047  prfval  18134  prfcl  18138  prf1st  18139  prf2nd  18140  1st2ndprf  18141  evlfcllem  18156  evlfcl  18157  curf1cl  18163  curfcl  18167  uncf1  18171  uncf2  18172  curfuncf  18173  uncfcurf  18174  diag1cl  18177  curf2ndf  18182  yon1cl  18198  oyon1cl  18206  yonedalem3a  18209  yonedalem4c  18212  yonedalem3b  18214  yonedalem3  18215  yonedainv  18216  yonffthlem  18217  yoniso  18220  func0g  49442  funchomf  49450  cofidf2a  49470  cofidf1a  49471  cofidf1  49474  imasubc  49504  imassc  49506  imaid  49507  imasubc3  49509  upciclem2  49520  upciclem3  49521  upeu2  49525  uppropd  49534  oppcup  49560  uptrlem1  49563  uptrlem3  49565  uptrar  49569  natoppf  49582  diag1  49657  diag1f1  49660  fuco111x  49684  fuco11idx  49688  fuco22natlem1  49695  fuco22natlem2  49696  fuco22natlem3  49697  fuco22natlem  49698  fucoid  49701  fuco23alem  49704  fucocolem1  49706  fucocolem2  49707  fucocolem3  49708  fucocolem4  49709  fucoco  49710  fucolid  49714  fucorid  49715  fucorid2  49716  precofvallem  49719  precofvalALT  49721  precofval2  49722  prcof22a  49745  prcofdiag1  49746  prcofdiag  49747  fucoppcco  49762  oppfdiag1  49767  oppfdiag  49769  functhincfun  49802  fullthinc  49803  thincciso2  49808  functermc  49861  fulltermc  49864  termcfuncval  49885  funcsn  49894  uobeqterm  49899  concom  50016  coccom  50017