Metamath Proof Explorer


Theorem setcthin

Description: A category of sets all of whose objects contain at most one element is thin. (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Hypotheses setcthin.c φC=SetCatU
setcthin.u φUV
setcthin.x φxU*ppx
Assertion setcthin Could not format assertion : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 setcthin.c φC=SetCatU
2 setcthin.u φUV
3 setcthin.x φxU*ppx
4 eqid SetCatU=SetCatU
5 4 2 setcbas φU=BaseSetCatU
6 eqidd φHomSetCatU=HomSetCatU
7 elequ2 x=zpxpz
8 7 mobidv x=z*ppx*ppz
9 3 adantr φyUzUxU*ppx
10 simprr φyUzUzU
11 8 9 10 rspcdva φyUzU*ppz
12 mofmo *ppz*ff:yz
13 11 12 syl φyUzU*ff:yz
14 2 adantr φyUzUUV
15 eqid HomSetCatU=HomSetCatU
16 simprl φyUzUyU
17 4 14 15 16 10 elsetchom φyUzUfyHomSetCatUzf:yz
18 17 mobidv φyUzU*ffyHomSetCatUz*ff:yz
19 13 18 mpbird φyUzU*ffyHomSetCatUz
20 4 setccat UVSetCatUCat
21 2 20 syl φSetCatUCat
22 5 6 19 21 isthincd Could not format ( ph -> ( SetCat ` U ) e. ThinCat ) : No typesetting found for |- ( ph -> ( SetCat ` U ) e. ThinCat ) with typecode |-
23 1 22 eqeltrd Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-