MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funcf1 Structured version   Visualization version   GIF version

Theorem funcf1 17855
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.
StepHypRef Expression
1 funcf1.f . . 3 (𝜑𝐹(𝐷 Func 𝐸)𝐺)
2 funcf1.b . . . 4 𝐵 = (Base‘𝐷)
3 funcf1.c . . . 4 𝐶 = (Base‘𝐸)
4 eqid 2725 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
5 eqid 2725 . . . 4 (Hom ‘𝐸) = (Hom ‘𝐸)
6 eqid 2725 . . . 4 (Id‘𝐷) = (Id‘𝐷)
7 eqid 2725 . . . 4 (Id‘𝐸) = (Id‘𝐸)
8 eqid 2725 . . . 4 (comp‘𝐷) = (comp‘𝐷)
9 eqid 2725 . . . 4 (comp‘𝐸) = (comp‘𝐸)
10 df-br 5150 . . . . . . 7 (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
111, 10sylib 217 . . . . . 6 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12 funcrcl 17852 . . . . . 6 (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1311, 12syl 17 . . . . 5 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1413simpld 493 . . . 4 (𝜑𝐷 ∈ Cat)
1513simprd 494 . . . 4 (𝜑𝐸 ∈ Cat)
162, 3, 4, 5, 6, 7, 8, 9, 14, 15isfunc 17853 . . 3 (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))(Hom ‘𝐸)(𝐹‘(2nd𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
171, 16mpbid 231 . 2 (𝜑 → (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))(Hom ‘𝐸)(𝐹‘(2nd𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
1817simp1d 1139 1 (𝜑𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3050  cop 4636   class class class wbr 5149   × cxp 5676  wf 6545  cfv 6549  (class class class)co 7419  1st c1st 7992  2nd c2nd 7993  m cmap 8845  Xcixp 8916  Basecbs 17183  Hom chom 17247  compcco 17248  Catccat 17647  Idccid 17648   Func cfunc 17843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-map 8847  df-ixp 8917  df-func 17847
This theorem is referenced by:  funcsect  17861  funcinv  17862  funciso  17863  funcoppc  17864  cofu1  17873  cofucl  17877  cofuass  17878  cofulid  17879  cofurid  17880  funcres  17885  funcres2  17887  wunfunc  17890  wunfuncOLD  17891  funcres2c  17893  fullpropd  17912  fthsect  17917  fthinv  17918  fthmon  17919  ffthiso  17921  cofull  17926  cofth  17927  fuccocl  17959  fucidcl  17960  fuclid  17961  fucrid  17962  fucass  17963  fucsect  17967  fucinv  17968  invfuc  17969  fuciso  17970  natpropd  17971  fucpropd  17972  catciso  18103  prfval  18193  prfcl  18197  prf1st  18198  prf2nd  18199  1st2ndprf  18200  evlfcllem  18216  evlfcl  18217  curf1cl  18223  curfcl  18227  uncf1  18231  uncf2  18232  curfuncf  18233  uncfcurf  18234  diag1cl  18237  curf2ndf  18242  yon1cl  18258  oyon1cl  18266  yonedalem3a  18269  yonedalem4c  18272  yonedalem3b  18274  yonedalem3  18275  yonedainv  18276  yonffthlem  18277  yoniso  18280  fullthinc  48238
  Copyright terms: Public domain W3C validator