Metamath Proof Explorer

Theorem thincciso2

Description: Categories isomorphic to a thin category are thin. Example 3.26(2) of Adamek p. 33. Note that "thincciso2.u" is redundant thanks to elbasfv . (Contributed by Zhi Wang, 18-Oct-2025)

Ref Expression
Hypotheses thincciso2.c 
|- C = ( CatCat ` U )
thincciso2.b 
|- B = ( Base ` C )
thincciso2.u 
|- ( ph -> U e. V )
thincciso2.x 
|- ( ph -> X e. B )
thincciso2.y 
|- ( ph -> Y e. B )
thincciso2.i 
|- I = ( Iso ` C )
thincciso2.f 
|- ( ph -> F e. ( X I Y ) )
thincciso2.yt 
|- ( ph -> Y e. ThinCat )
Assertion thincciso2 
|- ( ph -> X e. ThinCat )

Proof

Step Hyp Ref Expression
1 thincciso2.c 
 |-  C = ( CatCat ` U )
2 thincciso2.b 
 |-  B = ( Base ` C )
3 thincciso2.u 
 |-  ( ph -> U e. V )
4 thincciso2.x 
 |-  ( ph -> X e. B )
5 thincciso2.y 
 |-  ( ph -> Y e. B )
6 thincciso2.i 
 |-  I = ( Iso ` C )
7 thincciso2.f 
 |-  ( ph -> F e. ( X I Y ) )
8 thincciso2.yt 
 |-  ( ph -> Y e. ThinCat )
9 eqidd 
 |-  ( ph -> ( Base ` X ) = ( Base ` X ) )
10 eqidd 
 |-  ( ph -> ( Hom ` X ) = ( Hom ` X ) )
11 relfull 
 |-  Rel ( X Full Y )
12 relin1 
 |-  ( Rel ( X Full Y ) -> Rel ( ( X Full Y ) i^i ( X Faith Y ) ) )
13 11 12 ax-mp 
 |-  Rel ( ( X Full Y ) i^i ( X Faith Y ) )
14 eqid 
 |-  ( Base ` X ) = ( Base ` X )
15 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
16 1 2 14 15 3 4 5 6 catciso 
 |-  ( ph -> ( F e. ( X I Y ) <-> ( F e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` F ) : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) ) )
17 7 16 mpbid 
 |-  ( ph -> ( F e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` F ) : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) )
18 17 simpld 
 |-  ( ph -> F e. ( ( X Full Y ) i^i ( X Faith Y ) ) )
19 1st2ndbr 
 |-  ( ( Rel ( ( X Full Y ) i^i ( X Faith Y ) ) /\ F e. ( ( X Full Y ) i^i ( X Faith Y ) ) ) -> ( 1st ` F ) ( ( X Full Y ) i^i ( X Faith Y ) ) ( 2nd ` F ) )
20 13 18 19 sylancr 
 |-  ( ph -> ( 1st ` F ) ( ( X Full Y ) i^i ( X Faith Y ) ) ( 2nd ` F ) )
21 eqid 
 |-  ( Hom ` X ) = ( Hom ` X )
22 eqid 
 |-  ( Hom ` Y ) = ( Hom ` Y )
23 14 21 22 isffth2 
 |-  ( ( 1st ` F ) ( ( X Full Y ) i^i ( X Faith Y ) ) ( 2nd ` F ) <-> ( ( 1st ` F ) ( X Func Y ) ( 2nd ` F ) /\ A. x e. ( Base ` X ) A. y e. ( Base ` X ) ( x ( 2nd ` F ) y ) : ( x ( Hom ` X ) y ) -1-1-onto-> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) ) )
24 20 23 sylib 
 |-  ( ph -> ( ( 1st ` F ) ( X Func Y ) ( 2nd ` F ) /\ A. x e. ( Base ` X ) A. y e. ( Base ` X ) ( x ( 2nd ` F ) y ) : ( x ( Hom ` X ) y ) -1-1-onto-> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) ) )
25 24 simprd 
 |-  ( ph -> A. x e. ( Base ` X ) A. y e. ( Base ` X ) ( x ( 2nd ` F ) y ) : ( x ( Hom ` X ) y ) -1-1-onto-> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) )
26 25 r19.21bi 
 |-  ( ( ph /\ x e. ( Base ` X ) ) -> A. y e. ( Base ` X ) ( x ( 2nd ` F ) y ) : ( x ( Hom ` X ) y ) -1-1-onto-> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) )
27 26 r19.21bi 
 |-  ( ( ( ph /\ x e. ( Base ` X ) ) /\ y e. ( Base ` X ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` X ) y ) -1-1-onto-> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) )
28 27 anasss 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` X ) y ) -1-1-onto-> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) )
29 ovex 
 |-  ( x ( Hom ` X ) y ) e. _V
30 29 f1oen 
 |-  ( ( x ( 2nd ` F ) y ) : ( x ( Hom ` X ) y ) -1-1-onto-> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) -> ( x ( Hom ` X ) y ) ~~ ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) )
31 28 30 syl 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> ( x ( Hom ` X ) y ) ~~ ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) )
32 8 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> Y e. ThinCat )
33 24 simpld 
 |-  ( ph -> ( 1st ` F ) ( X Func Y ) ( 2nd ` F ) )
34 14 15 33 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` X ) --> ( Base ` Y ) )
35 34 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` X ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` Y ) )
36 35 adantrr 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` Y ) )
37 34 ffvelcdmda 
 |-  ( ( ph /\ y e. ( Base ` X ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` Y ) )
38 37 adantrl 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` Y ) )
39 32 36 38 15 22 thincmo 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> E* f f e. ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) )
40 modom2 
 |-  ( E* f f e. ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) <-> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) ~<_ 1o )
41 39 40 sylib 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) ~<_ 1o )
42 endomtr 
 |-  ( ( ( x ( Hom ` X ) y ) ~~ ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) /\ ( ( ( 1st ` F ) ` x ) ( Hom ` Y ) ( ( 1st ` F ) ` y ) ) ~<_ 1o ) -> ( x ( Hom ` X ) y ) ~<_ 1o )
43 31 41 42 syl2anc 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> ( x ( Hom ` X ) y ) ~<_ 1o )
44 modom2 
 |-  ( E* f f e. ( x ( Hom ` X ) y ) <-> ( x ( Hom ` X ) y ) ~<_ 1o )
45 43 44 sylibr 
 |-  ( ( ph /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) ) ) -> E* f f e. ( x ( Hom ` X ) y ) )
46 33 funcrcl2 
 |-  ( ph -> X e. Cat )
47 9 10 45 46 isthincd 
 |-  ( ph -> X e. ThinCat )