Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isthinc2 Structured version   Visualization version   GIF version

Theorem isthinc2 49419
Description: A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o. (Contributed by Zhi Wang, 17-Sep-2024.)
Hypotheses
Ref Expression
isthinc.b 𝐵 = (Base‘𝐶)
isthinc.h 𝐻 = (Hom ‘𝐶)
Assertion
Ref Expression
isthinc2 (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝐻𝑦) ≼ 1o))
Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐻,𝑦

Proof of Theorem isthinc2
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 isthinc.b . . 3 𝐵 = (Base‘𝐶)
2 isthinc.h . . 3 𝐻 = (Hom ‘𝐶)
31, 2isthinc 49418 . 2 (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥𝐵𝑦𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)))
4 modom2 9130 . . . 4 (∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦) ↔ (𝑥𝐻𝑦) ≼ 1o)
542ralbii 3104 . . 3 (∀𝑥𝐵𝑦𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦) ↔ ∀𝑥𝐵𝑦𝐵 (𝑥𝐻𝑦) ≼ 1o)
65anbi2i 623 . 2 ((𝐶 ∈ Cat ∧ ∀𝑥𝐵𝑦𝐵 ∃*𝑓 𝑓 ∈ (𝑥𝐻𝑦)) ↔ (𝐶 ∈ Cat ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝐻𝑦) ≼ 1o))
73, 6bitri 275 1 (𝐶 ∈ ThinCat ↔ (𝐶 ∈ Cat ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝐻𝑦) ≼ 1o))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wcel 2109  ∃*wmo 2531  wral 3044   class class class wbr 5088  cfv 6476  (class class class)co 7340  1oc1o 8372  cdom 8861  Basecbs 17107  Hom chom 17159  Catccat 17557  ThinCatcthinc 49416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pr 5367
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3393  df-v 3435  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7343  df-1o 8379  df-en 8864  df-dom 8865  df-sdom 8866  df-thinc 49417
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator