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

Theorem 0catg 17055
Description: Any structure with an empty set of objects is a category. (Contributed by Mario Carneiro, 3-Jan-2017.)
Assertion
Ref Expression
0catg ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ Cat)

Proof of Theorem 0catg
Dummy variables 𝑓 𝑔 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 488 . 2 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → ∅ = (Base‘𝐶))
2 eqidd 2739 . 2 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → (Hom ‘𝐶) = (Hom ‘𝐶))
3 eqidd 2739 . 2 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → (comp‘𝐶) = (comp‘𝐶))
4 simpl 486 . 2 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶𝑉)
5 noel 4217 . . . 4 ¬ 𝑥 ∈ ∅
65pm2.21i 119 . . 3 (𝑥 ∈ ∅ → ∅ ∈ (𝑥(Hom ‘𝐶)𝑥))
76adantl 485 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ 𝑥 ∈ ∅) → ∅ ∈ (𝑥(Hom ‘𝐶)𝑥))
8 simpr1 1195 . . 3 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))) → 𝑥 ∈ ∅)
95pm2.21i 119 . . 3 (𝑥 ∈ ∅ → (∅(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓)
108, 9syl 17 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))) → (∅(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓)
11 simpr1 1195 . . 3 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))) → 𝑥 ∈ ∅)
125pm2.21i 119 . . 3 (𝑥 ∈ ∅ → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)∅) = 𝑓)
1311, 12syl 17 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))) → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)∅) = 𝑓)
14 simp21 1207 . . 3 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ ∅)
155pm2.21i 119 . . 3 (𝑥 ∈ ∅ → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
1614, 15syl 17 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
17 simp2ll 1241 . . 3 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅) ∧ (𝑧 ∈ ∅ ∧ 𝑤 ∈ ∅)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤))) → 𝑥 ∈ ∅)
185pm2.21i 119 . . 3 (𝑥 ∈ ∅ → (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
1917, 18syl 17 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅) ∧ (𝑧 ∈ ∅ ∧ 𝑤 ∈ ∅)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤))) → (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
201, 2, 3, 4, 7, 10, 13, 16, 19iscatd 17040 1 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ Cat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1088   = wceq 1542  wcel 2113  c0 4209  cop 4519  cfv 6333  (class class class)co 7164  Basecbs 16579  Hom chom 16672  compcco 16673  Catccat 17031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-nul 5171
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-v 3399  df-sbc 3680  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-iota 6291  df-fv 6341  df-ov 7167  df-cat 17035
This theorem is referenced by:  0cat  17056  0thincg  45779
  Copyright terms: Public domain W3C validator