Theorem funcf1 18021

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 5104	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 221	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 18018	. . . . . 6 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
13	11, 12	syl 18	. . . . 5 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
14	13	simpld 500	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
15	13	simprd 501	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
16	2, 3, 4, 5, 6, 7, 8, 9, 14, 15	isfunc 18019	. . 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 1160	1 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ⟨cop 4590   class class class wbr 5103   × cxp 5649  ⟶wf 6527  ‘cfv 6531  (class class class)co 7412  1^st c1st 7988  2^nd c2nd 7989   ↑_m cmap 8831  Xcixp 8909  Basecbs 17367  Hom chom 17419  compcco 17420  Catccat 17818  Idccid 17819   Func cfunc 18009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8833  df-ixp 8910  df-func 18013

This theorem is used by:  funcsect  18027  funcinv  18028  funciso  18029  funcoppc  18030  cofu1  18039  cofucl  18043  cofuass  18044  cofulid  18045  cofurid  18046  funcres  18051  funcres2  18053  wunfunc  18056  funcres2c  18058  fullpropd  18077  fthsect  18082  fthinv  18083  fthmon  18084  ffthiso  18086  cofull  18091  cofth  18092  fuccocl  18122  fucidcl  18123  fuclid  18124  fucrid  18125  fucass  18126  fucsect  18130  fucinv  18131  invfuc  18132  fuciso  18133  natpropd  18134  fucpropd  18135  catciso  18266  prfval  18353  prfcl  18357  prf1st  18358  prf2nd  18359  1st2ndprf  18360  evlfcllem  18375  evlfcl  18376  curf1cl  18382  curfcl  18386  uncf1  18390  uncf2  18391  curfuncf  18392  uncfcurf  18393  diag1cl  18396  curf2ndf  18401  yon1cl  18417  oyon1cl  18425  yonedalem3a  18428  yonedalem4c  18431  yonedalem3b  18433  yonedalem3  18434  yonedainv  18435  yonffthlem  18436  yoniso  18439  func0g  50141  funchomf  50149  cofidf2a  50169  cofidf1a  50170  cofidf1  50173  imasubc  50203  imassc  50205  imaid  50206  imasubc3  50208  upciclem2  50219  upciclem3  50220  upeu2  50224  uppropd  50233  oppcup  50259  uptrlem1  50262  uptrlem3  50264  uptrar  50268  natoppf  50281  diag1  50356  diag1f1  50359  fuco111x  50383  fuco11idx  50387  fuco22natlem1  50394  fuco22natlem2  50395  fuco22natlem3  50396  fuco22natlem  50397  fucoid  50400  fuco23alem  50403  fucocolem1  50405  fucocolem2  50406  fucocolem3  50407  fucocolem4  50408  fucoco  50409  fucolid  50413  fucorid  50414  fucorid2  50415  precofvallem  50418  precofvalALT  50420  precofval2  50421  prcof22a  50444  prcofdiag1  50445  prcofdiag  50446  fucoppcco  50461  oppfdiag1  50466  oppfdiag  50468  functhincfun  50501  fullthinc  50502  thincciso2  50507  functermc  50560  fulltermc  50563  termcfuncval  50584  funcsn  50593  uobeqterm  50598  concom  50715  coccom  50716