This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 )