Theorem funcf1 17770

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 2731	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
5		eqid 2731	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
6		eqid 2731	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
7		eqid 2731	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
8		eqid 2731	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
9		eqid 2731	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
10		df-br 5092	. . . . . . 7 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
11	1, 10	sylib 218	. . . . . 6 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12		funcrcl 17767	. . . . . 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 17768	. . 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 1541   ∈ wcel 2111  ∀wral 3047  ⟨cop 4582   class class class wbr 5091   × cxp 5614  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346  1^st c1st 7919  2^nd c2nd 7920   ↑_m cmap 8750  Xcixp 8821  Basecbs 17117  Hom chom 17169  compcco 17170  Catccat 17567  Idccid 17568   Func cfunc 17758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-map 8752  df-ixp 8822  df-func 17762

This theorem is referenced by:  funcsect  17776  funcinv  17777  funciso  17778  funcoppc  17779  cofu1  17788  cofucl  17792  cofuass  17793  cofulid  17794  cofurid  17795  funcres  17800  funcres2  17802  wunfunc  17805  funcres2c  17807  fullpropd  17826  fthsect  17831  fthinv  17832  fthmon  17833  ffthiso  17835  cofull  17840  cofth  17841  fuccocl  17871  fucidcl  17872  fuclid  17873  fucrid  17874  fucass  17875  fucsect  17879  fucinv  17880  invfuc  17881  fuciso  17882  natpropd  17883  fucpropd  17884  catciso  18015  prfval  18102  prfcl  18106  prf1st  18107  prf2nd  18108  1st2ndprf  18109  evlfcllem  18124  evlfcl  18125  curf1cl  18131  curfcl  18135  uncf1  18139  uncf2  18140  curfuncf  18141  uncfcurf  18142  diag1cl  18145  curf2ndf  18150  yon1cl  18166  oyon1cl  18174  yonedalem3a  18177  yonedalem4c  18180  yonedalem3b  18182  yonedalem3  18183  yonedainv  18184  yonffthlem  18185  yoniso  18188  func0g  49120  funchomf  49128  cofidf2a  49148  cofidf1a  49149  cofidf1  49152  imasubc  49182  imassc  49184  imaid  49185  imasubc3  49187  upciclem2  49198  upciclem3  49199  upeu2  49203  uppropd  49212  oppcup  49238  uptrlem1  49241  uptrlem3  49243  uptrar  49247  natoppf  49260  diag1  49335  diag1f1  49338  fuco111x  49362  fuco11idx  49366  fuco22natlem1  49373  fuco22natlem2  49374  fuco22natlem3  49375  fuco22natlem  49376  fucoid  49379  fuco23alem  49382  fucocolem1  49384  fucocolem2  49385  fucocolem3  49386  fucocolem4  49387  fucoco  49388  fucolid  49392  fucorid  49393  fucorid2  49394  precofvallem  49397  precofvalALT  49399  precofval2  49400  prcof22a  49423  prcofdiag1  49424  prcofdiag  49425  fucoppcco  49440  oppfdiag1  49445  oppfdiag  49447  functhincfun  49480  fullthinc  49481  thincciso2  49486  functermc  49539  fulltermc  49542  termcfuncval  49563  funcsn  49572  uobeqterm  49577  concom  49694  coccom  49695