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	|- ( ph -> C = ( SetCat ` U ) )
	setcthin.u	|- ( ph -> U e. V )
	setcthin.x	|- ( ph -> A. x e. U E* p p e. x )
Assertion	setcthin	|- ( ph -> C e. ThinCat )

Proof

Step	Hyp	Ref	Expression
1		setcthin.c	|- ( ph -> C = ( SetCat ` U ) )
2		setcthin.u	|- ( ph -> U e. V )
3		setcthin.x	|- ( ph -> A. x e. U E* p p e. x )
4		eqid	|- ( SetCat ` U ) = ( SetCat ` U )
5	4 2	setcbas	|- ( ph -> U = ( Base ` ( SetCat ` U ) ) )
6		eqidd	|- ( ph -> ( Hom ` ( SetCat ` U ) ) = ( Hom ` ( SetCat ` U ) ) )
7		elequ2	|- ( x = z -> ( p e. x <-> p e. z ) )
8	7	mobidv	|- ( x = z -> ( E* p p e. x <-> E* p p e. z ) )
9	3	adantr	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> A. x e. U E* p p e. x )
10		simprr	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> z e. U )
11	8 9 10	rspcdva	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> E* p p e. z )
12		mofmo	|- ( E* p p e. z -> E* f f : y --> z )
13	11 12	syl	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> E* f f : y --> z )
14	2	adantr	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> U e. V )
15		eqid	|- ( Hom ` ( SetCat ` U ) ) = ( Hom ` ( SetCat ` U ) )
16		simprl	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> y e. U )
17	4 14 15 16 10	elsetchom	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> ( f e. ( y ( Hom ` ( SetCat ` U ) ) z ) <-> f : y --> z ) )
18	17	mobidv	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> ( E* f f e. ( y ( Hom ` ( SetCat ` U ) ) z ) <-> E* f f : y --> z ) )
19	13 18	mpbird	|- ( ( ph /\ ( y e. U /\ z e. U ) ) -> E* f f e. ( y ( Hom ` ( SetCat ` U ) ) z ) )
20	4	setccat	|- ( U e. V -> ( SetCat ` U ) e. Cat )
21	2 20	syl	|- ( ph -> ( SetCat ` U ) e. Cat )
22	5 6 19 21	isthincd	|- ( ph -> ( SetCat ` U ) e. ThinCat )
23	1 22	eqeltrd	|- ( ph -> C e. ThinCat )