Theorem funcf1 17822

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 5087	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 218	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 17819	. . . . . 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 17820	. . 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 4574   class class class wbr 5086   × cxp 5620  ⟶wf 6486  ‘cfv 6490  (class class class)co 7358  1^st c1st 7931  2^nd c2nd 7932   ↑_m cmap 8764  Xcixp 8836  Basecbs 17168  Hom chom 17220  compcco 17221  Catccat 17619  Idccid 17620   Func cfunc 17810

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 5212  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680

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 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8766  df-ixp 8837  df-func 17814

This theorem is referenced by:  funcsect  17828  funcinv  17829  funciso  17830  funcoppc  17831  cofu1  17840  cofucl  17844  cofuass  17845  cofulid  17846  cofurid  17847  funcres  17852  funcres2  17854  wunfunc  17857  funcres2c  17859  fullpropd  17878  fthsect  17883  fthinv  17884  fthmon  17885  ffthiso  17887  cofull  17892  cofth  17893  fuccocl  17923  fucidcl  17924  fuclid  17925  fucrid  17926  fucass  17927  fucsect  17931  fucinv  17932  invfuc  17933  fuciso  17934  natpropd  17935  fucpropd  17936  catciso  18067  prfval  18154  prfcl  18158  prf1st  18159  prf2nd  18160  1st2ndprf  18161  evlfcllem  18176  evlfcl  18177  curf1cl  18183  curfcl  18187  uncf1  18191  uncf2  18192  curfuncf  18193  uncfcurf  18194  diag1cl  18197  curf2ndf  18202  yon1cl  18218  oyon1cl  18226  yonedalem3a  18229  yonedalem4c  18232  yonedalem3b  18234  yonedalem3  18235  yonedainv  18236  yonffthlem  18237  yoniso  18240  func0g  49566  funchomf  49574  cofidf2a  49594  cofidf1a  49595  cofidf1  49598  imasubc  49628  imassc  49630  imaid  49631  imasubc3  49633  upciclem2  49644  upciclem3  49645  upeu2  49649  uppropd  49658  oppcup  49684  uptrlem1  49687  uptrlem3  49689  uptrar  49693  natoppf  49706  diag1  49781  diag1f1  49784  fuco111x  49808  fuco11idx  49812  fuco22natlem1  49819  fuco22natlem2  49820  fuco22natlem3  49821  fuco22natlem  49822  fucoid  49825  fuco23alem  49828  fucocolem1  49830  fucocolem2  49831  fucocolem3  49832  fucocolem4  49833  fucoco  49834  fucolid  49838  fucorid  49839  fucorid2  49840  precofvallem  49843  precofvalALT  49845  precofval2  49846  prcof22a  49869  prcofdiag1  49870  prcofdiag  49871  fucoppcco  49886  oppfdiag1  49891  oppfdiag  49893  functhincfun  49926  fullthinc  49927  thincciso2  49932  functermc  49985  fulltermc  49988  termcfuncval  50009  funcsn  50018  uobeqterm  50023  concom  50140  coccom  50141