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

Theorem 0catg 16701
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 479 . 2 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → ∅ = (Base‘𝐶))
2 eqidd 2827 . 2 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → (Hom ‘𝐶) = (Hom ‘𝐶))
3 eqidd 2827 . 2 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → (comp‘𝐶) = (comp‘𝐶))
4 simpl 476 . 2 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶𝑉)
5 noel 4149 . . . 4 ¬ 𝑥 ∈ ∅
65pm2.21i 117 . . 3 (𝑥 ∈ ∅ → ∅ ∈ (𝑥(Hom ‘𝐶)𝑥))
76adantl 475 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ 𝑥 ∈ ∅) → ∅ ∈ (𝑥(Hom ‘𝐶)𝑥))
8 simpr1 1254 . . 3 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))) → 𝑥 ∈ ∅)
95pm2.21i 117 . . 3 (𝑥 ∈ ∅ → (∅(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓)
108, 9syl 17 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))) → (∅(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓)
11 simpr1 1254 . . 3 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))) → 𝑥 ∈ ∅)
125pm2.21i 117 . . 3 (𝑥 ∈ ∅ → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)∅) = 𝑓)
1311, 12syl 17 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))) → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)∅) = 𝑓)
14 simp21 1269 . . 3 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ ∅)
155pm2.21i 117 . . 3 (𝑥 ∈ ∅ → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
1614, 15syl 17 . 2 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
17 simp2ll 1327 . . 3 (((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) ∧ ((𝑥 ∈ ∅ ∧ 𝑦 ∈ ∅) ∧ (𝑧 ∈ ∅ ∧ 𝑤 ∈ ∅)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤))) → 𝑥 ∈ ∅)
185pm2.21i 117 . . 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 16687 1 ((𝐶𝑉 ∧ ∅ = (Base‘𝐶)) → 𝐶 ∈ Cat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1113   = wceq 1658  wcel 2166  c0 4145  cop 4404  cfv 6124  (class class class)co 6906  Basecbs 16223  Hom chom 16317  compcco 16318  Catccat 16678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-nul 5014
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-iota 6087  df-fv 6132  df-ov 6909  df-cat 16682
This theorem is referenced by:  0cat  16702
  Copyright terms: Public domain W3C validator