Theorem funcf1 17882

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ⟨cop 4587   class class class wbr 5099   × cxp 5643  ⟶wf 6513  ‘cfv 6517  (class class class)co 7392  1^st c1st 7964  2^nd c2nd 7965   ↑_m cmap 8803  Xcixp 8875  Basecbs 17228  Hom chom 17280  compcco 17281  Catccat 17679  Idccid 17680   Func cfunc 17870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-map 8805  df-ixp 8876  df-func 17874

This theorem is referenced by:  funcsect  17888  funcinv  17889  funciso  17890  funcoppc  17891  cofu1  17900  cofucl  17904  cofuass  17905  cofulid  17906  cofurid  17907  funcres  17912  funcres2  17914  wunfunc  17917  funcres2c  17919  fullpropd  17938  fthsect  17943  fthinv  17944  fthmon  17945  ffthiso  17947  cofull  17952  cofth  17953  fuccocl  17983  fucidcl  17984  fuclid  17985  fucrid  17986  fucass  17987  fucsect  17991  fucinv  17992  invfuc  17993  fuciso  17994  natpropd  17995  fucpropd  17996  catciso  18127  prfval  18214  prfcl  18218  prf1st  18219  prf2nd  18220  1st2ndprf  18221  evlfcllem  18236  evlfcl  18237  curf1cl  18243  curfcl  18247  uncf1  18251  uncf2  18252  curfuncf  18253  uncfcurf  18254  diag1cl  18257  curf2ndf  18262  yon1cl  18278  oyon1cl  18286  yonedalem3a  18289  yonedalem4c  18292  yonedalem3b  18294  yonedalem3  18295  yonedainv  18296  yonffthlem  18297  yoniso  18300  func0g  49674  funchomf  49682  cofidf2a  49702  cofidf1a  49703  cofidf1  49706  imasubc  49736  imassc  49738  imaid  49739  imasubc3  49741  upciclem2  49752  upciclem3  49753  upeu2  49757  uppropd  49766  oppcup  49792  uptrlem1  49795  uptrlem3  49797  uptrar  49801  natoppf  49814  diag1  49889  diag1f1  49892  fuco111x  49916  fuco11idx  49920  fuco22natlem1  49927  fuco22natlem2  49928  fuco22natlem3  49929  fuco22natlem  49930  fucoid  49933  fuco23alem  49936  fucocolem1  49938  fucocolem2  49939  fucocolem3  49940  fucocolem4  49941  fucoco  49942  fucolid  49946  fucorid  49947  fucorid2  49948  precofvallem  49951  precofvalALT  49953  precofval2  49954  prcof22a  49977  prcofdiag1  49978  prcofdiag  49979  fucoppcco  49994  oppfdiag1  49999  oppfdiag  50001  functhincfun  50034  fullthinc  50035  thincciso2  50040  functermc  50093  fulltermc  50096  termcfuncval  50117  funcsn  50126  uobeqterm  50131  concom  50248  coccom  50249