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 2734	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2734	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2734	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2734	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2734	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2734	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 5124	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 218	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 17879	. . . . . 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 17880	. . 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 1539   ∈ wcel 2107  ∀wral 3050  ⟨cop 4612   class class class wbr 5123   × cxp 5663  ⟶wf 6537  ‘cfv 6541  (class class class)co 7413  1^st c1st 7994  2^nd c2nd 7995   ↑_m cmap 8848  Xcixp 8919  Basecbs 17229  Hom chom 17284  compcco 17285  Catccat 17678  Idccid 17679   Func cfunc 17870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-map 8850  df-ixp 8920  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  48891  upciclem2  48895  upciclem3  48896  upeu2  48900  oppcup  48919  diag1  48975  diag1f1  48978  fuco111x  49002  fuco11idx  49006  fuco22natlem1  49013  fuco22natlem2  49014  fuco22natlem3  49015  fuco22natlem  49016  fucoid  49019  fuco23alem  49022  fucocolem1  49024  fucocolem2  49025  fucocolem3  49026  fucocolem4  49027  fucoco  49028  fucolid  49032  fucorid  49033  fucorid2  49034  precofvallem  49037  precofvalALT  49039  precofval2  49040  functhincfun  49076  fullthinc  49077  thincciso2  49082  functermc  49121  fulltermc  49124  termcfuncval  49143