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

Theorem funcid 17802
Description: A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
funcid.b 𝐵 = (Base‘𝐷)
funcid.1 1 = (Id‘𝐷)
funcid.i 𝐼 = (Id‘𝐸)
funcid.f (𝜑𝐹(𝐷 Func 𝐸)𝐺)
funcid.x (𝜑𝑋𝐵)
Assertion
Ref Expression
funcid (𝜑 → ((𝑋𝐺𝑋)‘( 1𝑋)) = (𝐼‘(𝐹𝑋)))

Proof of Theorem funcid
Dummy variables 𝑚 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . 5 (𝑥 = 𝑋𝑥 = 𝑋)
21, 1oveq12d 7411 . . . 4 (𝑥 = 𝑋 → (𝑥𝐺𝑥) = (𝑋𝐺𝑋))
3 fveq2 6878 . . . 4 (𝑥 = 𝑋 → ( 1𝑥) = ( 1𝑋))
42, 3fveq12d 6885 . . 3 (𝑥 = 𝑋 → ((𝑥𝐺𝑥)‘( 1𝑥)) = ((𝑋𝐺𝑋)‘( 1𝑋)))
5 2fveq3 6883 . . 3 (𝑥 = 𝑋 → (𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑋)))
64, 5eqeq12d 2747 . 2 (𝑥 = 𝑋 → (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ↔ ((𝑋𝐺𝑋)‘( 1𝑋)) = (𝐼‘(𝐹𝑋))))
7 funcid.f . . . . 5 (𝜑𝐹(𝐷 Func 𝐸)𝐺)
8 funcid.b . . . . . 6 𝐵 = (Base‘𝐷)
9 eqid 2731 . . . . . 6 (Base‘𝐸) = (Base‘𝐸)
10 eqid 2731 . . . . . 6 (Hom ‘𝐷) = (Hom ‘𝐷)
11 eqid 2731 . . . . . 6 (Hom ‘𝐸) = (Hom ‘𝐸)
12 funcid.1 . . . . . 6 1 = (Id‘𝐷)
13 funcid.i . . . . . 6 𝐼 = (Id‘𝐸)
14 eqid 2731 . . . . . 6 (comp‘𝐷) = (comp‘𝐷)
15 eqid 2731 . . . . . 6 (comp‘𝐸) = (comp‘𝐸)
16 df-br 5142 . . . . . . . . 9 (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
177, 16sylib 217 . . . . . . . 8 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
18 funcrcl 17795 . . . . . . . 8 (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
1917, 18syl 17 . . . . . . 7 (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
2019simpld 495 . . . . . 6 (𝜑𝐷 ∈ Cat)
2119simprd 496 . . . . . 6 (𝜑𝐸 ∈ Cat)
228, 9, 10, 11, 12, 13, 14, 15, 20, 21isfunc 17796 . . . . 5 (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))(Hom ‘𝐸)(𝐹‘(2nd𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
237, 22mpbid 231 . . . 4 (𝜑 → (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))(Hom ‘𝐸)(𝐹‘(2nd𝑧))) ↑m ((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
2423simp3d 1144 . . 3 (𝜑 → ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))
25 simpl 483 . . . 4 ((((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))) → ((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)))
2625ralimi 3082 . . 3 (∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩(comp‘𝐸)(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))) → ∀𝑥𝐵 ((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)))
2724, 26syl 17 . 2 (𝜑 → ∀𝑥𝐵 ((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)))
28 funcid.x . 2 (𝜑𝑋𝐵)
296, 27, 28rspcdva 3610 1 (𝜑 → ((𝑋𝐺𝑋)‘( 1𝑋)) = (𝐼‘(𝐹𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3060  cop 4628   class class class wbr 5141   × cxp 5667  wf 6528  cfv 6532  (class class class)co 7393  1st c1st 7955  2nd c2nd 7956  m cmap 8803  Xcixp 8874  Basecbs 17126  Hom chom 17190  compcco 17191  Catccat 17590  Idccid 17591   Func cfunc 17786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-fv 6540  df-ov 7396  df-oprab 7397  df-mpo 7398  df-map 8805  df-ixp 8875  df-func 17790
This theorem is referenced by:  funcsect  17804  funcoppc  17807  cofucl  17820  funcres  17828  fthsect  17858  catcisolem  18042  prfcl  18137  evlfcl  18157  curf1cl  18163  curfcl  18167  curfuncf  18173  yonedainv  18216
  Copyright terms: Public domain W3C validator