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

Theorem catidex 16815
Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
catidex.b 𝐵 = (Base‘𝐶)
catidex.h 𝐻 = (Hom ‘𝐶)
catidex.o · = (comp‘𝐶)
catidex.c (𝜑𝐶 ∈ Cat)
catidex.x (𝜑𝑋𝐵)
Assertion
Ref Expression
catidex (𝜑 → ∃𝑔 ∈ (𝑋𝐻𝑋)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓))
Distinct variable groups:   𝑓,𝑔,𝑦,𝐵   𝐶,𝑓,𝑔,𝑦   𝜑,𝑔   𝑓,𝑋,𝑔,𝑦   𝑓,𝐻,𝑔,𝑦   · ,𝑓,𝑔,𝑦
Allowed substitution hints:   𝜑(𝑦,𝑓)

Proof of Theorem catidex
Dummy variables 𝑘 𝑤 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . 4 (𝑥 = 𝑋𝑥 = 𝑋)
21, 1oveq12d 6992 . . 3 (𝑥 = 𝑋 → (𝑥𝐻𝑥) = (𝑋𝐻𝑋))
3 oveq2 6982 . . . . . 6 (𝑥 = 𝑋 → (𝑦𝐻𝑥) = (𝑦𝐻𝑋))
4 opeq2 4674 . . . . . . . . 9 (𝑥 = 𝑋 → ⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑋⟩)
54, 1oveq12d 6992 . . . . . . . 8 (𝑥 = 𝑋 → (⟨𝑦, 𝑥· 𝑥) = (⟨𝑦, 𝑋· 𝑋))
65oveqd 6991 . . . . . . 7 (𝑥 = 𝑋 → (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = (𝑔(⟨𝑦, 𝑋· 𝑋)𝑓))
76eqeq1d 2773 . . . . . 6 (𝑥 = 𝑋 → ((𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓))
83, 7raleqbidv 3334 . . . . 5 (𝑥 = 𝑋 → (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓))
9 oveq1 6981 . . . . . 6 (𝑥 = 𝑋 → (𝑥𝐻𝑦) = (𝑋𝐻𝑦))
101, 1opeq12d 4681 . . . . . . . . 9 (𝑥 = 𝑋 → ⟨𝑥, 𝑥⟩ = ⟨𝑋, 𝑋⟩)
1110oveq1d 6989 . . . . . . . 8 (𝑥 = 𝑋 → (⟨𝑥, 𝑥· 𝑦) = (⟨𝑋, 𝑋· 𝑦))
1211oveqd 6991 . . . . . . 7 (𝑥 = 𝑋 → (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = (𝑓(⟨𝑋, 𝑋· 𝑦)𝑔))
1312eqeq1d 2773 . . . . . 6 (𝑥 = 𝑋 → ((𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓))
149, 13raleqbidv 3334 . . . . 5 (𝑥 = 𝑋 → (∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓))
158, 14anbi12d 622 . . . 4 (𝑥 = 𝑋 → ((∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)))
1615ralbidv 3140 . . 3 (𝑥 = 𝑋 → (∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)))
172, 16rexeqbidv 3335 . 2 (𝑥 = 𝑋 → (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑋𝐻𝑋)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)))
18 catidex.c . . 3 (𝜑𝐶 ∈ Cat)
19 catidex.b . . . . 5 𝐵 = (Base‘𝐶)
20 catidex.h . . . . 5 𝐻 = (Hom ‘𝐶)
21 catidex.o . . . . 5 · = (comp‘𝐶)
2219, 20, 21iscat 16813 . . . 4 (𝐶 ∈ Cat → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
2322ibi 259 . . 3 (𝐶 ∈ Cat → ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
24 simpl 475 . . . 4 ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) → ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
2524ralimi 3103 . . 3 (∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) → ∀𝑥𝐵𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
2618, 23, 253syl 18 . 2 (𝜑 → ∀𝑥𝐵𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
27 catidex.x . 2 (𝜑𝑋𝐵)
2817, 26, 27rspcdva 3534 1 (𝜑 → ∃𝑔 ∈ (𝑋𝐻𝑋)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1508  wcel 2051  wral 3081  wrex 3082  cop 4441  cfv 6185  (class class class)co 6974  Basecbs 16337  Hom chom 16430  compcco 16431  Catccat 16805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743  ax-nul 5063
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ral 3086  df-rex 3087  df-rab 3090  df-v 3410  df-sbc 3675  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-iota 6149  df-fv 6193  df-ov 6977  df-cat 16809
This theorem is referenced by:  catideu  16816
  Copyright terms: Public domain W3C validator