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	$$⊢\phi \to C=\mathrm{SetCat}\left(U\right)$$
	setcthin.u	$$⊢\phi \to U\in V$$
	setcthin.x	$$⊢\phi \to \forall x\in U{\exists }^{*}pp\in x$$
Assertion	setcthin	Could not format assertion : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		setcthin.c	$$⊢\phi \to C=\mathrm{SetCat}\left(U\right)$$
2		setcthin.u	$$⊢\phi \to U\in V$$
3		setcthin.x	$$⊢\phi \to \forall x\in U{\exists }^{*}pp\in x$$
4		eqid	$$⊢\mathrm{SetCat}\left(U\right)=\mathrm{SetCat}\left(U\right)$$
5	4 2	setcbas	$$⊢\phi \to U={\mathrm{Base}}_{\mathrm{SetCat}\left(U\right)}$$
6		eqidd	$$⊢\phi \to \mathrm{Hom}\left(\mathrm{SetCat}\left(U\right)\right)=\mathrm{Hom}\left(\mathrm{SetCat}\left(U\right)\right)$$
7		elequ2	$$⊢x=z\to \left(p\in x\leftrightarrow p\in z\right)$$
8	7	mobidv	$$⊢x=z\to \left({\exists }^{*}pp\in x\leftrightarrow {\exists }^{*}pp\in z\right)$$
9	3	adantr	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to \forall x\in U{\exists }^{*}pp\in x$$
10		simprr	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to z\in U$$
11	8 9 10	rspcdva	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to {\exists }^{*}pp\in z$$
12		mofmo	$$⊢{\exists }^{*}pp\in z\to {\exists }^{*}ff:y⟶z$$
13	11 12	syl	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to {\exists }^{*}ff:y⟶z$$
14	2	adantr	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to U\in V$$
15		eqid	$$⊢\mathrm{Hom}\left(\mathrm{SetCat}\left(U\right)\right)=\mathrm{Hom}\left(\mathrm{SetCat}\left(U\right)\right)$$
16		simprl	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to y\in U$$
17	4 14 15 16 10	elsetchom	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to \left(f\in \left(y\mathrm{Hom}\left(\mathrm{SetCat}\left(U\right)\right)z\right)\leftrightarrow f:y⟶z\right)$$
18	17	mobidv	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to \left({\exists }^{*}ff\in \left(y\mathrm{Hom}\left(\mathrm{SetCat}\left(U\right)\right)z\right)\leftrightarrow {\exists }^{*}ff:y⟶z\right)$$
19	13 18	mpbird	$$⊢\left(\phi \wedge \left(y\in U\wedge z\in U\right)\right)\to {\exists }^{*}ff\in \left(y\mathrm{Hom}\left(\mathrm{SetCat}\left(U\right)\right)z\right)$$
20	4	setccat	$$⊢U\in V\to \mathrm{SetCat}\left(U\right)\in \mathrm{Cat}$$
21	2 20	syl	$$⊢\phi \to \mathrm{SetCat}\left(U\right)\in \mathrm{Cat}$$
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 |-