Theorem funcf1 18070

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 2763	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2763	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2763	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2763	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2763	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2763	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 5107	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 221	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 18067	. . . . . 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 18068	. . 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 2147  ∀wral 3080  ⟨cop 4838   class class class wbr 5106   × cxp 5653  ⟶wf 6554  ‘cfv 6558  (class class class)co 7443  1^st c1st 8023  2^nd c2nd 8024   ↑_m cmap 8875  Xcixp 8953  Basecbs 17416  Hom chom 17468  compcco 17469  Catccat 17867  Idccid 17868   Func cfunc 18058

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-map 8877  df-ixp 8954  df-func 18062

This theorem is used by:  funcsect  18076  funcinv  18077  funciso  18078  funcoppc  18079  cofu1  18088  cofucl  18092  cofuass  18093  cofulid  18094  cofurid  18095  funcres  18100  funcres2  18102  wunfunc  18105  funcres2c  18107  fullpropd  18126  fthsect  18131  fthinv  18132  fthmon  18133  ffthiso  18135  cofull  18140  cofth  18141  fuccocl  18171  fucidcl  18172  fuclid  18173  fucrid  18174  fucass  18175  fucsect  18179  fucinv  18180  invfuc  18181  fuciso  18182  natpropd  18183  fucpropd  18184  catciso  18315  prfval  18402  prfcl  18406  prf1st  18407  prf2nd  18408  1st2ndprf  18409  evlfcllem  18424  evlfcl  18425  curf1cl  18431  curfcl  18435  uncf1  18439  uncf2  18440  curfuncf  18441  uncfcurf  18442  diag1cl  18445  curf2ndf  18450  yon1cl  18466  oyon1cl  18474  yonedalem3a  18477  yonedalem4c  18480  yonedalem3b  18482  yonedalem3  18483  yonedainv  18484  yonffthlem  18485  yoniso  18488  func0g  50409  cofu1stfix  50417  funchomf  50418  cofidf2a  50438  cofidf1a  50439  cofidf1  50442  imasubc  50472  imassc  50474  imaid  50475  imasubc3  50477  upciclem2  50488  upciclem3  50489  upeu2  50493  uppropd  50502  oppcup  50528  uptrlem1  50531  uptrlem3  50533  uptrar  50537  natideq  50550  natoppf  50556  diag1  50631  diag1f1  50634  fuco111x  50658  fuco11idx  50662  fuco22natlem1  50669  fuco22natlem2  50670  fuco22natlem3  50671  fuco22natlem  50672  fucoid  50675  fuco23alem  50678  fucocolem1  50680  fucocolem2  50681  fucocolem3  50682  fucocolem4  50683  fucoco  50684  fucolid  50688  fucorid  50689  fucorid2  50690  precofvallem  50706  precofvalALT  50708  precofval2  50709  prcof22a  50732  prcofdiag1  50733  prcofdiag  50734  fucoppcco  50749  oppfdiag1  50754  oppfdiag  50756  functhincfun  50789  fullthinc  50790  thincciso2  50795  functermc  50848  fulltermc  50851  termcfuncval  50872  termccofix  50876  funcsn  50884  uobeqterm  50889  concom  51051  coccom  51052