Theorem funcf1 17913

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ⟨cop 4591   class class class wbr 5105   × cxp 5650  ⟶wf 6521  ‘cfv 6525  (class class class)co 7400  1^st c1st 7972  2^nd c2nd 7973   ↑_m cmap 8812  Xcixp 8883  Basecbs 17259  Hom chom 17311  compcco 17312  Catccat 17710  Idccid 17711   Func cfunc 17901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-map 8814  df-ixp 8884  df-func 17905

This theorem is referenced by:  funcsect  17919  funcinv  17920  funciso  17921  funcoppc  17922  cofu1  17931  cofucl  17935  cofuass  17936  cofulid  17937  cofurid  17938  funcres  17943  funcres2  17945  wunfunc  17948  funcres2c  17950  fullpropd  17969  fthsect  17974  fthinv  17975  fthmon  17976  ffthiso  17978  cofull  17983  cofth  17984  fuccocl  18014  fucidcl  18015  fuclid  18016  fucrid  18017  fucass  18018  fucsect  18022  fucinv  18023  invfuc  18024  fuciso  18025  natpropd  18026  fucpropd  18027  catciso  18158  prfval  18245  prfcl  18249  prf1st  18250  prf2nd  18251  1st2ndprf  18252  evlfcllem  18267  evlfcl  18268  curf1cl  18274  curfcl  18278  uncf1  18282  uncf2  18283  curfuncf  18284  uncfcurf  18285  diag1cl  18288  curf2ndf  18293  yon1cl  18309  oyon1cl  18317  yonedalem3a  18320  yonedalem4c  18323  yonedalem3b  18325  yonedalem3  18326  yonedainv  18327  yonffthlem  18328  yoniso  18331  func0g  49718  funchomf  49726  cofidf2a  49746  cofidf1a  49747  cofidf1  49750  imasubc  49780  imassc  49782  imaid  49783  imasubc3  49785  upciclem2  49796  upciclem3  49797  upeu2  49801  uppropd  49810  oppcup  49836  uptrlem1  49839  uptrlem3  49841  uptrar  49845  natoppf  49858  diag1  49933  diag1f1  49936  fuco111x  49960  fuco11idx  49964  fuco22natlem1  49971  fuco22natlem2  49972  fuco22natlem3  49973  fuco22natlem  49974  fucoid  49977  fuco23alem  49980  fucocolem1  49982  fucocolem2  49983  fucocolem3  49984  fucocolem4  49985  fucoco  49986  fucolid  49990  fucorid  49991  fucorid2  49992  precofvallem  49995  precofvalALT  49997  precofval2  49998  prcof22a  50021  prcofdiag1  50022  prcofdiag  50023  fucoppcco  50038  oppfdiag1  50043  oppfdiag  50045  functhincfun  50078  fullthinc  50079  thincciso2  50084  functermc  50137  fulltermc  50140  termcfuncval  50161  funcsn  50170  uobeqterm  50175  concom  50292  coccom  50293