Theorem funcf1 17791

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 2729	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2729	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2729	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2729	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2729	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2729	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 5096	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 218	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 17788	. . . . . 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 17789	. . 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 1142	1 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ⟨cop 4585   class class class wbr 5095   × cxp 5621  ⟶wf 6482  ‘cfv 6486  (class class class)co 7353  1^st c1st 7929  2^nd c2nd 7930   ↑_m cmap 8760  Xcixp 8831  Basecbs 17138  Hom chom 17190  compcco 17191  Catccat 17588  Idccid 17589   Func cfunc 17779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-map 8762  df-ixp 8832  df-func 17783

This theorem is referenced by:  funcsect  17797  funcinv  17798  funciso  17799  funcoppc  17800  cofu1  17809  cofucl  17813  cofuass  17814  cofulid  17815  cofurid  17816  funcres  17821  funcres2  17823  wunfunc  17826  funcres2c  17828  fullpropd  17847  fthsect  17852  fthinv  17853  fthmon  17854  ffthiso  17856  cofull  17861  cofth  17862  fuccocl  17892  fucidcl  17893  fuclid  17894  fucrid  17895  fucass  17896  fucsect  17900  fucinv  17901  invfuc  17902  fuciso  17903  natpropd  17904  fucpropd  17905  catciso  18036  prfval  18123  prfcl  18127  prf1st  18128  prf2nd  18129  1st2ndprf  18130  evlfcllem  18145  evlfcl  18146  curf1cl  18152  curfcl  18156  uncf1  18160  uncf2  18161  curfuncf  18162  uncfcurf  18163  diag1cl  18166  curf2ndf  18171  yon1cl  18187  oyon1cl  18195  yonedalem3a  18198  yonedalem4c  18201  yonedalem3b  18203  yonedalem3  18204  yonedainv  18205  yonffthlem  18206  yoniso  18209  func0g  49075  funchomf  49083  cofidf2a  49103  cofidf1a  49104  cofidf1  49107  imasubc  49137  imassc  49139  imaid  49140  imasubc3  49142  upciclem2  49153  upciclem3  49154  upeu2  49158  uppropd  49167  oppcup  49193  uptrlem1  49196  uptrlem3  49198  uptrar  49202  natoppf  49215  diag1  49290  diag1f1  49293  fuco111x  49317  fuco11idx  49321  fuco22natlem1  49328  fuco22natlem2  49329  fuco22natlem3  49330  fuco22natlem  49331  fucoid  49334  fuco23alem  49337  fucocolem1  49339  fucocolem2  49340  fucocolem3  49341  fucocolem4  49342  fucoco  49343  fucolid  49347  fucorid  49348  fucorid2  49349  precofvallem  49352  precofvalALT  49354  precofval2  49355  prcof22a  49378  prcofdiag1  49379  prcofdiag  49380  fucoppcco  49395  oppfdiag1  49400  oppfdiag  49402  functhincfun  49435  fullthinc  49436  thincciso2  49441  functermc  49494  fulltermc  49497  termcfuncval  49518  funcsn  49527  uobeqterm  49532  concom  49649  coccom  49650