Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  setcthin Structured version   Visualization version   GIF version
Theorem setcthin 47228
Description: A category of sets all of whose objects contain at most one element is thin. (Contributed by Zhi Wang, 20-Sep-2024.)
Hypotheses
Ref Expression
setcthin.c (πœ‘ β†’ 𝐢 = (SetCatβ€˜π‘ˆ))
setcthin.u (πœ‘ β†’ π‘ˆ ∈ 𝑉)
setcthin.x (πœ‘ β†’ βˆ€π‘₯ ∈ π‘ˆ βˆƒ*𝑝 𝑝 ∈ π‘₯)
Assertion
Ref Expression
setcthin (πœ‘ β†’ 𝐢 ∈ ThinCat)
Distinct variable group:   π‘ˆ,𝑝,π‘₯
Allowed substitution hints:   πœ‘(π‘₯,𝑝)   𝐢(π‘₯,𝑝)   𝑉(π‘₯,𝑝)
Proof of Theorem setcthin
Dummy variables 𝑓 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 setcthin.c . 2 (πœ‘ β†’ 𝐢 = (SetCatβ€˜π‘ˆ))
2 eqid 2731 . . . 4 (SetCatβ€˜π‘ˆ) = (SetCatβ€˜π‘ˆ)
3 setcthin.u . . . 4 (πœ‘ β†’ π‘ˆ ∈ 𝑉)
42, 3setcbas 17993 . . 3 (πœ‘ β†’ π‘ˆ = (Baseβ€˜(SetCatβ€˜π‘ˆ)))
5 eqidd 2732 . . 3 (πœ‘ β†’ (Hom β€˜(SetCatβ€˜π‘ˆ)) = (Hom β€˜(SetCatβ€˜π‘ˆ)))
6 elequ2 2121 . . . . . . 7 (π‘₯ = 𝑧 β†’ (𝑝 ∈ π‘₯ ↔ 𝑝 ∈ 𝑧))
76mobidv 2542 . . . . . 6 (π‘₯ = 𝑧 β†’ (βˆƒ*𝑝 𝑝 ∈ π‘₯ ↔ βˆƒ*𝑝 𝑝 ∈ 𝑧))
8 setcthin.x . . . . . . 7 (πœ‘ β†’ βˆ€π‘₯ ∈ π‘ˆ βˆƒ*𝑝 𝑝 ∈ π‘₯)
98adantr 481 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ βˆ€π‘₯ ∈ π‘ˆ βˆƒ*𝑝 𝑝 ∈ π‘₯)
10 simprr 771 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ 𝑧 ∈ π‘ˆ)
117, 9, 10rspcdva 3596 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ βˆƒ*𝑝 𝑝 ∈ 𝑧)
12 mofmo 47066 . . . . 5 (βˆƒ*𝑝 𝑝 ∈ 𝑧 β†’ βˆƒ*𝑓 𝑓:π‘¦βŸΆπ‘§)
1311, 12syl 17 . . . 4 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ βˆƒ*𝑓 𝑓:π‘¦βŸΆπ‘§)
143adantr 481 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ π‘ˆ ∈ 𝑉)
15 eqid 2731 . . . . . 6 (Hom β€˜(SetCatβ€˜π‘ˆ)) = (Hom β€˜(SetCatβ€˜π‘ˆ))
16 simprl 769 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ 𝑦 ∈ π‘ˆ)
172, 14, 15, 16, 10elsetchom 17996 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ (𝑓 ∈ (𝑦(Hom β€˜(SetCatβ€˜π‘ˆ))𝑧) ↔ 𝑓:π‘¦βŸΆπ‘§))
1817mobidv 2542 . . . 4 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ (βˆƒ*𝑓 𝑓 ∈ (𝑦(Hom β€˜(SetCatβ€˜π‘ˆ))𝑧) ↔ βˆƒ*𝑓 𝑓:π‘¦βŸΆπ‘§))
1913, 18mpbird 256 . . 3 ((πœ‘ ∧ (𝑦 ∈ π‘ˆ ∧ 𝑧 ∈ π‘ˆ)) β†’ βˆƒ*𝑓 𝑓 ∈ (𝑦(Hom β€˜(SetCatβ€˜π‘ˆ))𝑧))
202setccat 18000 . . . 4 (π‘ˆ ∈ 𝑉 β†’ (SetCatβ€˜π‘ˆ) ∈ Cat)
213, 20syl 17 . . 3 (πœ‘ β†’ (SetCatβ€˜π‘ˆ) ∈ Cat)
224, 5, 19, 21isthincd 47210 . 2 (πœ‘ β†’ (SetCatβ€˜π‘ˆ) ∈ ThinCat)
231, 22eqeltrd 2832 1 (πœ‘ β†’ 𝐢 ∈ ThinCat)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆƒ*wmo 2531  βˆ€wral 3060  βŸΆwf 6512  β€˜cfv 6516  (class class class)co 7377  Hom chom 17173  Catccat 17573  SetCatcsetc 17990  ThinCatcthinc 47192
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 5262  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  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-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3364  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-pss 3947  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-uni 4886  df-iun 4976  df-br 5126  df-opab 5188  df-mpt 5209  df-tr 5243  df-id 5551  df-eprel 5557  df-po 5565  df-so 5566  df-fr 5608  df-we 5610  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-pred 6273  df-ord 6340  df-on 6341  df-lim 6342  df-suc 6343  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7333  df-ov 7380  df-oprab 7381  df-mpo 7382  df-om 7823  df-1st 7941  df-2nd 7942  df-frecs 8232  df-wrecs 8263  df-recs 8337  df-rdg 8376  df-1o 8432  df-er 8670  df-map 8789  df-en 8906  df-dom 8907  df-sdom 8908  df-fin 8909  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11411  df-neg 11412  df-nn 12178  df-2 12240  df-3 12241  df-4 12242  df-5 12243  df-6 12244  df-7 12245  df-8 12246  df-9 12247  df-n0 12438  df-z 12524  df-dec 12643  df-uz 12788  df-fz 13450  df-struct 17045  df-slot 17080  df-ndx 17092  df-base 17110  df-hom 17186  df-cco 17187  df-cat 17577  df-cid 17578  df-setc 17991  df-thinc 47193
This theorem is referenced by:  setc2othin  47229
  Copyright terms: Public domain W3C validator