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

Theorem funcf1 16728
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 2804 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
5 eqid 2804 . . . 4 (Hom ‘𝐸) = (Hom ‘𝐸)
6 eqid 2804 . . . 4 (Id‘𝐷) = (Id‘𝐷)
7 eqid 2804 . . . 4 (Id‘𝐸) = (Id‘𝐸)
8 eqid 2804 . . . 4 (comp‘𝐷) = (comp‘𝐷)
9 eqid 2804 . . . 4 (comp‘𝐸) = (comp‘𝐸)
10 df-br 4843 . . . . . . 7 (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
111, 10sylib 209 . . . . . 6 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
12 funcrcl 16725 . . . . . 6 (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1311, 12syl 17 . . . . 5 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1413simpld 484 . . . 4 (𝜑𝐷 ∈ Cat)
1513simprd 485 . . . 4 (𝜑𝐸 ∈ Cat)
162, 3, 4, 5, 6, 7, 8, 9, 14, 15isfunc 16726 . . 3 (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))(Hom ‘𝐸)(𝐹‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
171, 16mpbid 223 . 2 (𝜑 → (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))(Hom ‘𝐸)(𝐹‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘((Id‘𝐷)‘𝑥)) = ((Id‘𝐸)‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
1817simp1d 1165 1 (𝜑𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wcel 2156  wral 3094  cop 4374   class class class wbr 4842   × cxp 5307  wf 6095  cfv 6099  (class class class)co 6872  1st c1st 7394  2nd c2nd 7395  𝑚 cmap 8090  Xcixp 8143  Basecbs 16066  Hom chom 16162  compcco 16163  Catccat 16527  Idccid 16528   Func cfunc 16716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5094  ax-un 7177
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-ral 3099  df-rex 3100  df-reu 3101  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-iun 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-id 5217  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-res 5321  df-ima 5322  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-ov 6875  df-oprab 6876  df-mpt2 6877  df-map 8092  df-ixp 8144  df-func 16720
This theorem is referenced by:  funcsect  16734  funcinv  16735  funciso  16736  funcoppc  16737  cofu1  16746  cofucl  16750  cofuass  16751  cofulid  16752  cofurid  16753  funcres  16758  funcres2  16760  wunfunc  16761  funcres2c  16763  fullpropd  16782  fthsect  16787  fthinv  16788  fthmon  16789  ffthiso  16791  cofull  16796  cofth  16797  fuccocl  16826  fucidcl  16827  fuclid  16828  fucrid  16829  fucass  16830  fucsect  16834  fucinv  16835  invfuc  16836  fuciso  16837  natpropd  16838  fucpropd  16839  catciso  16959  prfval  17042  prfcl  17046  prf1st  17047  prf2nd  17048  1st2ndprf  17049  evlfcllem  17064  evlfcl  17065  curf1cl  17071  curfcl  17075  uncf1  17079  uncf2  17080  curfuncf  17081  uncfcurf  17082  diag1cl  17085  curf2ndf  17090  yon1cl  17106  oyon1cl  17114  yonedalem3a  17117  yonedalem4c  17120  yonedalem3b  17122  yonedalem3  17123  yonedainv  17124  yonffthlem  17125  yoniso  17128
  Copyright terms: Public domain W3C validator